X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fnat_ordered_set.ma;h=231cdf941aacb8b28d1230535901f2f691f978ef;hb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;hp=6ecbe5424fc8810ab201dce248fd45520e96c90d;hpb=9f064ffe2834ae91f306b44f79bfbfb68a4631c5;p=helm.git

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 6ecbe5424..231cdf941 100644
--- 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,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
-
 include "nat/compare.ma".
-include "cprop_connectives.ma". 
+include "bishop_set.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -27,6 +25,7 @@ intros 5;elim n; [apply H]
 cases m;[ apply H1| apply H2; apply H3 ]
 qed.
 
+alias symbol "lt" = "natural 'less than'".
 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
 intros (x y); apply (nat_elim2 ???? x y); 
 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
@@ -50,14 +49,28 @@ apply (mk_ordered_set ? nat_excess);
 |2: apply nat_excess_cotransitive]
 qed.
 
-alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+interpretation "ordered set N" 'N = nat_ordered_set.
+
+alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
 lemma os_le_to_nat_le:
-  ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
+  ∀a,b:nat_ordered_set.a ≤ b → le a b.
 intros; normalize in H; apply (not_lt_to_le ?? H);
 qed.
  
 lemma nat_le_to_os_le:
-  ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
+  ∀a,b:nat_ordered_set.le a b → a ≤ b.
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
-  
\ No newline at end of file
+
+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