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

diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
index 4f3631cdb..1d375df88 100644
--- a/helm/software/matita/library/nat/factorial2.ma
+++ b/helm/software/matita/library/nat/factorial2.ma
@@ -25,20 +25,21 @@ theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
 intros.reflexivity.
 qed.
 
-lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
+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 fact1: \forall n.
-fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
-intro.elim n
-  [rewrite < times_n_O.apply le_n
+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
+  [apply le_n
   |rewrite > times_SSO.
    rewrite > factS.
    rewrite > factS.
    rewrite < assoc_times.
    rewrite > factS.
-   apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
+   apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
     [apply le_times_l.
      rewrite > times_SSO.
      apply le_times_r.
@@ -46,6 +47,7 @@ intro.elim n
     |rewrite > assoc_times.
      rewrite > assoc_times.
      rewrite > assoc_times in ⊢ (? ? %).
+     change in ⊢ (? ? (? (? ? %) ?)) with (S(2*n1)).
      rewrite > exp_S. 
      rewrite > assoc_times in ⊢ (? ? %).
      apply le_times_r.
@@ -54,26 +56,42 @@ intro.elim n
      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
      rewrite > assoc_times.
      rewrite > assoc_times.
-     rewrite > exp_S. 
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite > sym_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite < assoc_times in ⊢ (? ? %).
-     rewrite < assoc_times in ⊢ (? ? %).
-     rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite > sym_times in ⊢ (? ? (? ? %)).
-     rewrite > sym_times in ⊢ (? ? %).
-     assumption
+     rewrite > S_pred in ⊢ (? ? (? (? ? %) ?))
+      [rewrite > exp_S. 
+       rewrite > assoc_times in ⊢ (? ? %).
+       apply le_times_r.
+       rewrite > sym_times in ⊢ (? ? %).
+       rewrite > assoc_times in ⊢ (? ? %).
+       rewrite > assoc_times in ⊢ (? ? %).
+       apply le_times_r.
+       rewrite < assoc_times in ⊢ (? ? %).
+       rewrite < assoc_times in ⊢ (? ? %).
+       rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
+       rewrite > assoc_times in ⊢ (? ? %).
+       rewrite > assoc_times in ⊢ (? ? %).
+       apply le_times_r.
+       rewrite > sym_times in ⊢ (? ? (? ? %)).
+       rewrite > sym_times in ⊢ (? ? %).
+       assumption
+      |unfold.rewrite > times_n_SO in ⊢ (? % ?).
+       apply le_times
+        [apply le_n_Sn
+        |assumption
+        ]
+      ]
     ]
   ]
 qed.
 
+theorem fact1: \forall n.
+fact (2*n) \le (exp 2 (pred (2*n)))*(fact n)*(fact n).
+intro.cases n
+  [apply le_n
+  |apply lt_O_to_fact1.
+   apply lt_O_S
+  ]
+qed.
+
 theorem lt_O_fact: \forall n. O < fact n.
 intro.elim n
   [simplify.apply lt_O_S
@@ -140,6 +158,45 @@ intros.elim H
   ]
 qed.
 
+(* 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).
+intros.
+elim H
+  [simplify.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite < times_exp.
+   change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
+   rewrite > assoc_times.
+   rewrite > assoc_times in ⊢ (? (? ? %) ?).
+   rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
+   rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
+    [apply le_times_r.
+     apply le_times_r.
+     apply le_times_r.
+     assumption
+    |rewrite > factS.
+     rewrite > factS.
+     rewrite < times_SSO.
+     rewrite > assoc_times in ⊢ (? ? %). 
+     apply le_times_r.
+     rewrite < assoc_times.
+     change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
+     rewrite < assoc_times in ⊢ (? (? % ?) ?).
+     rewrite < times_n_SO.
+     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < assoc_times in ⊢ (? ? (? % ?)).
+     apply le_times_r.
+     apply le_times_l.
+     apply le_S.apply le_n
+    ]
+  ]
+qed.
+
 (*
 theorem stirling: \forall n,k.k \le n \to
 log (fact n) < n*log n - n + k*log n.