snapshot

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 85f686da3ebed0968b3e7970ee599d3fb552b9a5..1b34801d2949e2516096675c462066eeed18d7d1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -16,8 +16,18 @@
 include "sandwich.ma".
 include "property_exhaustivity.ma".
 
-le x_i e y_i stanno o no nel segmento?
-
+lemma foo:
+  ∀C:ordered_set.
+   ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.∀p:a order_converges x. 
+       ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j).
+intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
+cases H2; clear H2;  intro; cases (H5 ? H2);
+cases (H (w2+j)); apply (H8 H6);
+qed.   
+     
+     
 (* Theorem 3.10 *)
 theorem lebesgue:
   ∀C:ordered_uniform_space.
@@ -34,7 +44,8 @@ theorem lebesgue:
 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; 
 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
 split;
-[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
+[2: intro h;
+  cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
 
 
 (* Theorem 3.9 *)

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index 691d21045957d285b230c08bb82ee45984fad487..f6a315c82e8db48cbdccf74b975b7e367c2cad74 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -112,7 +112,10 @@ lapply (H9 ?? H10) as H11; [
   apply (trans_increasing ?? H4); intro; whd in H12;
   apply (not_le_Sn_n i);  apply (transitive_le ??? H12 H5)]
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m p));
+generalize in match (refl_eq nat (m p)); 
+(*
+intro E; cases p in E : (? ? ? ?);
+*)
 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
 intros (H16); simplify in H16:(? ? ? %); destruct H16;
 apply H15; [3: apply le_n]