X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;h=2a1089fec45188916b69bfd8659df83030afcf49;hb=6abb01e8b00db927e16aa790354d1da57af7875b;hp=a4b40be7a4ba844f3d774583e5890a9561862ec5;hpb=c33fae30b4ce40198b8e1889ea1c1b58697cd567;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a4b40be7a..2a1089fec 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -36,6 +36,7 @@ record half_ordered_set: Type ≝ {
 
 definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O). 
 
+(*
 lemma find_leq : half_ordered_set → half_ordered_set.
 intro O; constructor 1;
 [1: apply (hos_carr O);
@@ -49,6 +50,7 @@ intro O; constructor 1;
     rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
     [assumption] cases Hletin;[right|left]assumption;]
 qed.
+*)
 
 definition dual_hos : half_ordered_set → half_ordered_set.
 intro; constructor 1;
@@ -75,8 +77,6 @@ intro hos;
 constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] 
 qed.
 
-(* coercion half2full. *)
-  
 definition Type_of_ordered_set : ordered_set → Type.
 intro o; apply (hos_carr (os_l o)); qed.