From b58b7f9f3fdf8d66522b31828faa5bfa588c31b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 18:20:20 +0000 Subject: [PATCH] generalize no more required before elim --- helm/software/matita/library/nat/minus.ma | 7 +++---- helm/software/matita/library/nat/neper.ma | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index a0133e93d..10d218d44 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -76,13 +76,12 @@ qed. theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m. intros 2. -generalize in match n. -elim m. +elim m in n ⊢ %. rewrite < minus_n_O.apply plus_n_O. -elim n2.simplify. +elim n1.simplify. apply minus_n_n. rewrite < plus_n_Sm. -change with (S n3 = (S n3 + n1)-n1). +change with (S n2 = (S n2 + n)-n). apply H. qed. diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 8e70ab958..ab14a9ab4 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -902,7 +902,7 @@ intros;apply eq_sigma_p;intros; |apply (inj_times_r (pred ((n-x)!))); rewrite < (S_pred ((n-x)!)) [rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?); - rewrite < H3;generalize in match H2;elim x + rewrite < H3;generalize in match H2; elim x [rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity |rewrite < fact_minus in H4; [rewrite > true_to_pi_p_Sn -- 2.39.2