X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ffactorial2.ma;h=6215d6657892ab39eb0233763885657f35796725;hb=3f5a0152427fd9a89e7239befd259d27b97aaef5;hp=1d375df88a364fbf575f57cc1781e78482088bc7;hpb=173965d294635f861850a850769b1530c73b835f;p=helm.git

diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
index 1d375df88..6215d6657 100644
--- a/helm/software/matita/library/nat/factorial2.ma
+++ b/helm/software/matita/library/nat/factorial2.ma
@@ -25,11 +25,6 @@ theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
 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
@@ -197,6 +192,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.