From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 7 Jun 2008 09:57:28 +0000 (+0000)
Subject: proof simplified
X-Git-Tag: make_still_working~5066
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=012011414a61185b1c90467413206d12cf8fc2f5;p=helm.git

proof simplified
---

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index c67dd1785..9d87b28d5 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -114,16 +114,10 @@ lapply (H9 ?? H10) as H11; [
   apply (trans_increasing ?? H4); intro; whd in H12;
   apply (not_le_Sn_n i);  apply (transitive_le ??? H12 H5)]
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m q)); 
-generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?)); 
-generalize in match (refl_eq nat (m r)); 
-generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %)); 
 generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H16:(? ? ? %);
-apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
+intros (H16); simplify in H16:(? ? ? %); destruct H16;
+apply H15; [3: apply le_n]
 [1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
     apply (le_to_not_lt p q H5);
 |2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]