Another bug.

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

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 48551f85e70ab95c2867e65d4aea9b1e93fcd919..7145b42886c802cc4d75574a77e3c64906e357ea 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -19,10 +19,10 @@ lemma h_segment_upperbound:
   ∀C:half_ordered_set.
    ∀s:segment C.
     ∀a:sequence (half_segment_ordered_set C s).
-     (seg_u C s) (upper_bound ? ⌊n,\fst (a n)⌋). 
-intros; cases (wloss_prop C); unfold; rewrite < H; simplify; intro n;
-cases (a n); simplify; unfold in H1; rewrite < H in H1; cases H1; 
-simplify in H2 H3; rewrite < H in H2 H3; assumption;
+      upper_bound ? ⌊n,\fst (a n)⌋ (seg_u C s). 
+intros 4; simplify; cases (a n); simplify; unfold in H;
+cases (wloss_prop C); rewrite < H1 in H; simplify; cases H; 
+assumption;
 qed.
 
 notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
@@ -68,13 +68,6 @@ definition exhaustive ≝
      (a is_increasing → a is_upper_located → a is_cauchy) ∧
      (b is_decreasing → b is_lower_located → b is_cauchy).
 
-lemma prove_in_segment: 
- ∀O:half_ordered_set.∀s:segment O.∀x:O.
-   seg_l O s (λl.l ≤≤ x) → seg_u O s (λu.x ≤≤ u) → x ∈ s.
-intros; unfold; cases (wloss_prop O); rewrite < H2;
-split; assumption;
-qed.
-
 lemma h_uparrow_to_in_segment:
   ∀C:half_ordered_set.
    ∀s:segment C.
@@ -83,15 +76,15 @@ lemma h_uparrow_to_in_segment:
        ∀x:C. uparrow C a x → 
          in_segment C s x.
 intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
-cases (wloss_prop C) (W W); apply prove_in_segment; unfold; rewrite <W;simplify;
+cases (wloss_prop C) (W W); apply prove_in_segment; unfold; 
 [ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite <W in K;
-  cases K; unfold in H4 H6; rewrite <W in H6 H4; simplify in H4 H6; assumption;
+  cases K; unfold in H4 H6; apply H4;
 | intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
-  cases K; unfold in H5 H4; rewrite<W in H4 H5; simplify in H4 H5; apply (H5 H6);    
+  cases K; unfold in H5 H4; apply H5; apply H6;    
 | apply (hle_transitive ??? x ?  (H2 O)); lapply (H1 0) as K; unfold in K; rewrite <W in K;
-  cases K; unfold in H4 H6; rewrite <W in H4 H6; simplify in H4 H6; assumption;
+  cases K; unfold in H4 H6; apply H6;
 | intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
-  cases K; unfold in H5 H4; rewrite<W in H4 H5; simplify in H4 H5; apply (H4 H6);]    
+  cases K; unfold in H5 H4; apply (H4 H6);]    
 qed.
 
 notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.