Some improvement.

diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
index 1d375df88a364fbf575f57cc1781e78482088bc7..594feb51f7ec365fe4ea568f9723c2e33d489c13 100644 (file)
--- a/helm/software/matita/library/nat/factorial2.ma
+++ b/helm/software/matita/library/nat/factorial2.ma
@@ -197,6 +197,83 @@ elim H
   ]
 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.