Binomial coefficients and costant e.

[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
new file mode 100644 (file)
index 0000000..e618ec5
--- /dev/null
+++ b/helm/software/matita/library/nat/neper.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       __                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/neper".
+
+include "nat/iteration2.ma".
+include "nat/div_and_mod_diseq.ma".
+
+theorem boh: \forall n,m.
+sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le 
+((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
+intros.
+elim n
+  [apply le_O_n.
+  |rewrite > true_to_sigma_p_Sn
+    [apply (trans_le ? (m/(S(S O))\sup(n1)+((S(S O))*m*(S(S O))\sup(n1)-(S(S O))*m)/(S(S O))\sup(n1)))
+      [apply le_plus_r.assumption
+      |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
+       rewrite < distr_times_minus.
+       change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
+       rewrite > sym_times in ⊢ (? ? (? % ?)).
+       rewrite > sym_times in ⊢ (? ? (? ? %)).
+       rewrite < lt_to_lt_to_eq_div_div_times_times
+        [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
+          [apply le_plus_div.
+           apply lt_O_exp.
+           apply lt_O_S
+          |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
+           rewrite < plus_n_O.
+           rewrite < eq_minus_minus_minus_plus.
+           rewrite > sym_plus.
+           rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
+           rewrite > assoc_times.
+           rewrite < plus_minus_m_m
+            [apply le_n
+            |apply le_plus_to_minus_r.
+             rewrite > plus_n_O in ⊢ (? (? ? %) ?).
+             change in ⊢ (? % ?) with ((S(S O))*m). 
+             rewrite > sym_times.
+             apply le_times_r.
+             rewrite > times_n_SO in ⊢ (? % ?).
+             apply le_times_r.
+             apply lt_O_exp.
+             apply lt_O_S
+            ]
+          ]
+        |apply lt_O_S
+        |apply lt_O_exp.
+         apply lt_O_S
+        ]
+      ]
+    |reflexivity
+    ]
+  ]
+qed.
+   
\ No newline at end of file