From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 3 Jun 2008 08:12:57 +0000 (+0000)
Subject: proof refactored
X-Git-Tag: make_still_working~5091
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20c68603cc71aeb957d5e974558d908f2261fb6d;p=helm.git

proof refactored
---

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 40026abc2..65d43ac18 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -104,15 +104,12 @@ intros; elim w;
     cases H1; [exists [apply O] apply H2;]
     exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p)); 
-    [ cases H2; clear H2;
-      [ exists [apply p]; assumption;
-      | exists [apply (S p)]; rewrite > H3; apply H;]
-    | cases (?:False); change in Hp with (n<m p);
-apply (not_le_Sn_n (m p) ?).
- apply (transitive_le (S (m p)) (S n) (m p) ? ?);
-  [apply (H2).
-  |apply (Hp).
-  ]]]
+    [1: cases H2; clear H2;
+        [1: exists [apply p]; assumption;
+        |2: exists [apply (S p)]; rewrite > H3; apply H;]
+    |2: cases (?:False); change in Hp with (n<m p);
+        apply (not_le_Sn_n (m p));
+        apply (transitive_le ??? H2 Hp);]]
 qed.
      
 lemma selection: 
@@ -125,5 +122,5 @@ intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
     cases (strictly_increasing_reaches C ? Hm w); 
     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]  
     cases (trans_increasing C ? Ia ?? H1); assumption;]
-qed. (* dovevo usare il lemma 2.3! *)     
+qed.