(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/factorial2".
-
include "nat/exp.ma".
include "nat/factorial.ma".
intros.reflexivity.
qed.
-alias num (instance 0) = "natural number".
-lemma times_SSO: \forall n.2*(S n) = S(S(2*n)).
-intro.simplify.rewrite < plus_n_Sm.reflexivity.
-qed.
-
theorem lt_O_to_fact1: \forall n.O<n \to
fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
intros.elim H
qed.
theorem fact2: \forall n.O < n \to
-(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
+(exp 2 (2*n))*(fact n)*(fact n) < fact (S(2*n)).
intros.elim H
[simplify.apply le_S.apply le_n
|rewrite > times_SSO.
(* a slightly better result *)
theorem fact3: \forall n.O < n \to
-(exp (S(S O)) ((S(S O))*n))*(exp (fact n) (S(S O))) \le (S(S O))*n*fact ((S(S O))*n).
+(exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
intros.
elim H
[simplify.apply le_n