Restructuring.

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

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f3db405d42f09b63c8a9378b481075934d667d59..4b90420c8f78bc913499bdc476acfffb4fbf1b14 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -195,7 +195,22 @@ apply lt_sigma_p
   ]
 qed.
        
-   
+theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O))).
+intro.  
+apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
+  [apply le_exp_sigma_p_exp
+  |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) i))))
+    [apply le_sigma_p.intros.
+     apply le_times_to_le_div
+      [apply lt_O_exp.
+       apply lt_O_S
+      |apply (trans_le ? ((S(S O))\sup i* n \sup n/i!))
+        [apply le_times_div_div_times.
+         apply lt_O_fact
+        |apply le_times_to_le_div2
+          [apply lt_O_fact
+          |rewrite < sym_times.
+           apply le_times_r.