gran casino

[helm.git] / helm / software / matita / contribs / dama / dama / nat_ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 6ecbe5424fc8810ab201dce248fd45520e96c90d..18ecf8e6027f7ca5ada1011dfb45825d4fc84b4e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -12,10 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
-
+include "bishop_set.ma". 
 include "nat/compare.ma".
-include "cprop_connectives.ma". 
+include "cprop_connectives.ma".
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -60,4 +59,17 @@ lemma nat_le_to_os_le:
   ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
-  
\ No newline at end of file
+
+alias id "lt" = "cic:/matita/dama/bishop_set/lt.con".
+lemma nat_lt_to_os_lt:
+  ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
+intros 3; split;
+[1: apply nat_le_to_os_le; apply lt_to_le;assumption;
+|2: right; apply H;]
+qed.
+
+lemma os_lt_to_nat_lt:
+  ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
+intros; cases H; clear H; cases H2;
+[2: apply H;| cases (H1 H)]
+qed.
\ No newline at end of file