X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fsigma_and_pi.ma;h=4f5f6cba008299370b94fb0e95f7b0b6248407a6;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=331df8fb3c4fa426b369d770604dff0ec90f1eb7;hpb=fcc4e47ab6406a9a666471e017b81cf364195866;p=helm.git

diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index 331df8fb3..4f5f6cba0 100644
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -36,8 +36,8 @@ intros 3.elim n.
 simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
 apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
 apply H.intros.apply H1.assumption.
 rewrite < plus_n_Sm.
 apply le_S.assumption.
@@ -51,8 +51,8 @@ intros 3.elim n.
 simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
 apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
 apply H.intros.apply H1.assumption.
 rewrite < plus_n_Sm.
 apply le_S.assumption.
@@ -61,7 +61,7 @@ qed.
 theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
 intro.elim n.
 simplify.reflexivity.
-change with (S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O)).
+change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))).
 rewrite < plus_n_Sm.rewrite < plus_n_O.
 apply eq_f.assumption.
 qed.