helm/software/matita/library/nat/neper.ma

   1 (**************************************************************************)
   2 (*       __                                                               *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/neper".
  16
  17 include "nat/iteration2.ma".
  18 include "nat/div_and_mod_diseq.ma".
  19
  20 theorem boh: \forall n,m.
  21 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  22 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  23 intros.
  24 elim n
  25   [apply le_O_n.
  26   |rewrite > true_to_sigma_p_Sn
  27     [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)))
  28       [apply le_plus_r.assumption
  29       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  30        rewrite < distr_times_minus.
  31        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  32        rewrite > sym_times in ⊢ (? ? (? % ?)).
  33        rewrite > sym_times in ⊢ (? ? (? ? %)).
  34        rewrite < lt_to_lt_to_eq_div_div_times_times
  35         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  36           [apply le_plus_div.
  37            apply lt_O_exp.
  38            apply lt_O_S
  39           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  40            rewrite < plus_n_O.
  41            rewrite < eq_minus_minus_minus_plus.
  42            rewrite > sym_plus.
  43            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  44            rewrite > assoc_times.
  45            rewrite < plus_minus_m_m
  46             [apply le_n
  47             |apply le_plus_to_minus_r.
  48              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  49              change in ⊢ (? % ?) with ((S(S O))*m).
  50              rewrite > sym_times.
  51              apply le_times_r.
  52              rewrite > times_n_SO in ⊢ (? % ?).
  53              apply le_times_r.
  54              apply lt_O_exp.
  55              apply lt_O_S
  56             ]
  57           ]
  58         |apply lt_O_S
  59         |apply lt_O_exp.
  60          apply lt_O_S
  61         ]
  62       ]
  63     |reflexivity
  64     ]
  65   ]
  66 qed.
  67