ordered_set simplified

[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 56b354859ad2521bc94a30f458adf29b3b3ad72e..890164ea950d405fd295ad26e0227d62b68d42e7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -36,22 +36,6 @@ 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);
-|2: apply (λT:Type.λf:T→T→CProp.f); 
-|3: intros; left; intros; reflexivity;
-|4: apply (hos_excess_ O);
-|5: intro x; lapply (hos_coreflexive O x) as H; cases (wloss_prop O);
-    rewrite < H1 in H; apply H;
-|6: intros 4 (x y z H); cases (wloss_prop O);
-    rewrite > (H1 ? (hos_excess_ O)) in H ⊢ %; 
-    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;
 [ apply (hos_carr h);
@@ -64,9 +48,7 @@ intro; constructor 1;
 qed.
 
 record ordered_set : Type ≝ {
-  os_l : half_ordered_set;
-  os_r_ : half_ordered_set;
-  os_with : os_r_ = dual_hos os_l
+  os_l : half_ordered_set
 }.
 
 definition os_r : ordered_set → half_ordered_set.
@@ -74,7 +56,7 @@ intro o; apply (dual_hos (os_l o)); qed.
 
 lemma half2full : half_ordered_set → ordered_set.
 intro hos;
-constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] 
+constructor 1; apply hos;  
 qed.
 
 definition Type_of_ordered_set : ordered_set → Type.
@@ -183,10 +165,7 @@ apply (mk_half_ordered_set (O × O));
 qed.
 
 lemma square_ordered_set: ordered_set → ordered_set.
-intro O; constructor 1;
-[ apply (square_half_ordered_set (os_l O));
-| apply (dual_hos (square_half_ordered_set (os_l O)));
-| reflexivity]
+intro O; constructor 1; apply (square_half_ordered_set (os_l O));
 qed.
 
 notation "s 2 \atop \nleq" non associative with precedence 90