proof refactored

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 40026abc266bad2b9ba231c97bbfec0634fd6936..65d43ac18d3f62be9278426b008e4a2b08a5e2db 100644 (file)
--- 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.