From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Jun 2008 08:53:45 +0000 (+0000)
Subject: better names in a lemma to increase readability
X-Git-Tag: make_still_working~5036
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f79c94ded2ae71654374b9b28c1c8b9a63a651ac;p=helm.git

better names in a lemma to increase readability
---

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 46fe6e422..dcf59e2aa 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -21,10 +21,11 @@ lemma order_converges_bigger_lowsegment:
    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.∀p:a order_converges x. 
        ∀j.l ≤ (fst p) j.
-intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
-cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
-intro H2; cases (H8 ? H2);
-cases (H (w1+j)); apply (H12 H7);
+intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
+cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
+cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
+intro H2; cases (SSa ? H2) (w Hw); simplify in Hw;
+cases (H (w+j)) (Hal Hau); apply (Hau Hw);
 qed.   
 
 lemma order_converges_smaller_upsegment: