X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=ab14a9ab45857b6d65194307ac74e747b7754fd9;hb=b58b7f9f3fdf8d66522b31828faa5bfa588c31b8;hp=8e70ab958c9a462c7573b447077a99de629f2979;hpb=dc0aa21dae28cd07142cb7bcaf8e6a1bfd99018d;p=helm.git

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