From 012011414a61185b1c90467413206d12cf8fc2f5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 7 Jun 2008 09:57:28 +0000 Subject: [PATCH] proof simplified --- .../matita/contribs/dama/dama/property_sigma.ma | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) 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;] -- 2.39.2