(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/sigma_and_pi".
+set "baseuri" "cic:/matita/library_autobatch/nat/sigma_and_pi".
include "auto/nat/factorial.ma".
include "auto/nat/exp.ma".
intros 3.
elim n
[ simplify.
- auto
+ autobatch
(*apply H
[ apply le_n
| rewrite < plus_n_O.
| simplify.
apply eq_f2
[ apply H1
- [ auto
+ [ autobatch
(*change with (m \le (S n1)+m).
apply le_plus_n*)
- | auto
+ | autobatch
(*rewrite > (sym_plus m).
apply le_n*)
]
intros.
apply H1
[ assumption
- | auto
+ | autobatch
(*rewrite < plus_n_Sm.
apply le_S.
assumption*)
intros 3.
elim n
[ simplify.
- auto
+ autobatch
(*apply H
[ apply le_n
| rewrite < plus_n_O.
| simplify.
apply eq_f2
[ apply H1
- [ auto
+ [ autobatch
(*change with (m \le (S n1)+m).
apply le_plus_n*)
- | auto
+ | autobatch
(*rewrite > (sym_plus m).
apply le_n*)
]
intros.
apply H1
[ assumption
- | auto
+ | autobatch
(*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
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| 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.
- auto
+ autobatch
(*apply eq_f.
assumption*)
]
(exp a (S n))*pi n f m= pi n (\lambda p.a*(f p)) m.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
rewrite < times_n_SO.
reflexivity*)
apply eq_f.
rewrite < assoc_times.
rewrite < assoc_times.
- auto
+ autobatch
(*apply eq_f2
[ apply sym_times
| reflexivity