lebesge works

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

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a4b40be7a4ba844f3d774583e5890a9561862ec5..2a1089fec45188916b69bfd8659df83030afcf49 100644 (file)
--- 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.