From 20c68603cc71aeb957d5e974558d908f2261fb6d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 3 Jun 2008 08:12:57 +0000
Subject: [PATCH] proof refactored

---
 .../matita/contribs/dama/dama/supremum.ma       | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

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.     
     
-- 
2.39.2