Improved approximations

[helm.git] / helm / software / matita / library / nat / factorial2.ma

diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
index dd3df52d4952bbe5e4c3bfe4efe40df3fa11b653..1d375df88a364fbf575f57cc1781e78482088bc7 100644 (file)
--- 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