(* *)
(**************************************************************************)
-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
]
qed.
+theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
+simplify in \vdash (? (? %) ?).
+rewrite > factS in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+apply le_times_l.
+apply leb_true_to_le.reflexivity.
+qed.
+
+theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
+intros.
+rewrite > assoc_times.
+rewrite > assoc_times.
+apply eq_f.
+rewrite < assoc_times.
+rewrite < assoc_times.
+rewrite > sym_times in \vdash (? ? (? % ?) ?).
+reflexivity.
+qed.
+
+(* an even better result *)
+theorem lt_SSSSO_to_fact: \forall n.4<n \to
+fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
+intros.elim H
+ [apply le_fact_10
+ |rewrite > times_SSO.
+ change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
+ rewrite < minus_n_O.
+ rewrite > factS.
+ rewrite > factS.
+ rewrite < assoc_times.
+ rewrite > factS.
+ apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
+ [apply le_times_l.
+ rewrite > times_SSO.
+ apply le_times_r.
+ apply le_n_Sn
+ |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
+ [apply le_times_r.assumption
+ |rewrite > assoc_times.
+ rewrite > ab_times_cd in \vdash (? (? ? %) ?).
+ rewrite < assoc_times.
+ apply le_times_l.
+ rewrite < assoc_times in \vdash (? (? ? %) ?).
+ rewrite > ab_times_cd.
+ apply le_times_l.
+ rewrite < exp_S.
+ rewrite < exp_S.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite > eq_minus_S_pred.
+ rewrite < S_pred
+ [rewrite > eq_minus_S_pred.
+ rewrite < S_pred
+ [rewrite < minus_n_O.
+ apply le_n
+ |elim H1;simplify
+ [apply lt_O_S
+ |apply lt_O_S
+ ]
+ ]
+ |elim H1;simplify
+ [apply lt_O_S
+ |rewrite < plus_n_Sm.
+ rewrite < minus_n_O.
+ apply lt_O_S
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+
(*
theorem stirling: \forall n,k.k \le n \to
log (fact n) < n*log n - n + k*log n.