generalize no more required before elim

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index a0133e93db58f65df22e64ca4e94944a26fda79e..10d218d440d7194f2d10e127fddcc3f9eadff05e 100644 (file)
--- 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 8e70ab958c9a462c7573b447077a99de629f2979..ab14a9ab45857b6d65194307ac74e747b7754fd9 100644 (file)
--- 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