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.
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.
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.