X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fnat_ordered_set.ma;h=dfeaa6d35074c8cddc99f7798a332ba8bdc21b66;hb=c231702a57076acf0c161cdb4799bf83158175f0;hp=d4aa1d57d18780367e650b63dc9ad37eb0109a72;hpb=bf7f52019b3f65b6d635a8b49a63f0d95080f189;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 d4aa1d57d..dfeaa6d35 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -44,8 +44,9 @@ cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
 qed.
   
 lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat nat_excess ? nat_excess_cotransitive);[
-  intro x; intro H; apply (not_le_Sn_n ? H);]
+letin hos ≝ (mk_half_ordered_set nat (λT:Type.λf:T→T→CProp.f) ? nat_excess ? nat_excess_cotransitive);
+[ intros; left; intros; reflexivity;
+| intro x; intro H; apply (not_le_Sn_n ? H);]
 constructor 1;  
 [ apply hos; | apply (dual_hos hos); | reflexivity]
 qed.
@@ -63,17 +64,3 @@ lemma nat_le_to_os_le:
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
 
-(*
-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