Bertrand's conjecture (weak), some work in progress

[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 4f3631cdbd06a3893a97843a2c325323474b250a..dd3df52d4952bbe5e4c3bfe4efe40df3fa11b653 100644 (file)
--- a/helm/software/matita/library/nat/factorial2.ma
+++ b/helm/software/matita/library/nat/factorial2.ma
@@ -140,6 +140,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.