X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fnat_ordered_set.ma;h=6ecbe5424fc8810ab201dce248fd45520e96c90d;hb=9f064ffe2834ae91f306b44f79bfbfb68a4631c5;hp=e7dfec46152d1ef9cb32951cc9e7a4df2bfc8f4e;hpb=2cb6a7c755375fa6b64a3590ebc98957829afdca;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 e7dfec461..6ecbe5424 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -15,7 +15,7 @@
 include "ordered_set.ma".
 
 include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "cprop_connectives.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -49,3 +49,15 @@ apply (mk_ordered_set ? nat_excess);
 [1: intro x; intro; apply (not_le_Sn_n ? H);
 |2: apply nat_excess_cotransitive]
 qed.
+
+alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+lemma os_le_to_nat_le:
+  ∀a,b:nat_ordered_set.le nat_ordered_set a b → 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.
+intros 3; apply (le_to_not_lt a b);assumption;
+qed.
+  
\ No newline at end of file