(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/factorial".
+set "baseuri" "cic:/matita/library_autobatch/nat/factorial".
include "auto/nat/le_arith.ma".
[ O \Rightarrow (S O)
| (S m) \Rightarrow (S m)*(fact m)].
-interpretation "factorial" 'fact n = (cic:/matita/library_auto/nat/factorial/fact.con n).
+interpretation "factorial" 'fact n = (cic:/matita/library_autobatch/nat/factorial/fact.con n).
theorem le_SO_fact : \forall n. (S O) \le n!.
intro.
elim n
-[ auto
+[ autobatch
(*simplify.
apply le_n*)
| change with ((S O) \le (S n1)*n1!).
- auto
+ autobatch
(*apply (trans_le ? ((S n1)*(S O)))
[ simplify.
apply le_S_S.
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_le_Sn_O (S O) H).*)
| intros.
change with ((S (S O)) \le (S m)*m!).
- apply (trans_le ? ((S(S O))*(S O)));auto
+ apply (trans_le ? ((S(S O))*(S O)));autobatch
(*[ apply le_n
| apply le_times
[ exact H
elim n
[ apply le_O_n
| change with (S n1 \le (S n1)*n1!).
- apply (trans_le ? ((S n1)*(S O)));auto
+ apply (trans_le ? ((S n1)*(S O)));autobatch
(*[ rewrite < times_n_SO.
apply le_n
| apply le_times.
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_le_Sn_O (S(S O)) H)*)
| intros.
simplify.
unfold lt.
apply le_S_S.
- auto
+ autobatch
(*rewrite < plus_n_O.
apply le_plus_n*)
| apply le_times_r.
- auto
+ autobatch
(*apply le_SSO_fact.
simplify.
unfold lt.