From f79c94ded2ae71654374b9b28c1c8b9a63a651ac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Jun 2008 08:53:45 +0000 Subject: [PATCH] better names in a lemma to increase readability --- helm/software/matita/contribs/dama/dama/lebesgue.ma | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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: -- 2.39.2