From c38c15fa800498bcac6230e07a31ed54414a0865 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 10 Dec 2007 14:24:40 +0000
Subject: [PATCH] Main result for e.

---
 helm/software/matita/library/nat/neper.ma | 46 +++++++++++++++++++++--
 1 file changed, 43 insertions(+), 3 deletions(-)

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 4b90420c8..fe9b7ac1a 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -194,23 +194,63 @@ apply lt_sigma_p
     ]
   ]
 qed.
+
+theorem le_exp_SSO_fact:\forall n. 
+exp (S(S O)) (pred n) \le n!.
+intro.elim n
+  [apply le_n
+  |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
+   apply (nat_case1 n1);intros
+    [apply le_n
+    |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
+     apply le_times
+      [apply le_S_S.apply le_S_S.apply le_O_n
+      |rewrite < H1.assumption
+      ]
+    ]
+  ]
+qed.
        
-theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O))).
+theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O)))*(exp n n).
 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 (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred 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 (trans_le ? ((S(S O))\sup (pred 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.
+           apply le_exp_SSO_fact
+          ]
+        ]
+      ]
+    |rewrite > eq_sigma_p_pred
+      [rewrite > div_SO.
+       rewrite > sym_plus.
+       change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
+       apply le_plus_r.
+       apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
+        [apply sigma_p_div_exp
+        |apply le_times_to_le_div2
+          [apply lt_O_exp.
+           apply lt_O_S.
+          |apply le_minus_m
+          ]
+        ]
+      |reflexivity
+      ]
+    ]
+  ]
+qed.
+    
+      
     
 
    
-- 
2.39.2