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 include "nat/binomial.ma".
  20 include "nat/log.ma".
  21 include "nat/chebyshev.ma".
  22
  23 theorem sigma_p_div_exp: \forall n,m.
  24 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  25 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  26 intros.
  27 elim n
  28   [apply le_O_n.
  29   |rewrite > true_to_sigma_p_Sn
  30     [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)))
  31       [apply le_plus_r.assumption
  32       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  33        rewrite < distr_times_minus.
  34        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  35        rewrite > sym_times in ⊢ (? ? (? % ?)).
  36        rewrite > sym_times in ⊢ (? ? (? ? %)).
  37        rewrite < lt_to_lt_to_eq_div_div_times_times
  38         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  39           [apply le_plus_div.
  40            apply lt_O_exp.
  41            apply lt_O_S
  42           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  43            rewrite < plus_n_O.
  44            rewrite < eq_minus_minus_minus_plus.
  45            rewrite > sym_plus.
  46            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  47            rewrite > assoc_times.
  48            rewrite < plus_minus_m_m
  49             [apply le_n
  50             |apply le_plus_to_minus_r.
  51              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  52              change in ⊢ (? % ?) with ((S(S O))*m).
  53              rewrite > sym_times.
  54              apply le_times_r.
  55              rewrite > times_n_SO in ⊢ (? % ?).
  56              apply le_times_r.
  57              apply lt_O_exp.
  58              apply lt_O_S
  59             ]
  60           ]
  61         |apply lt_O_S
  62         |apply lt_O_exp.
  63          apply lt_O_S
  64         ]
  65       ]
  66     |reflexivity
  67     ]
  68   ]
  69 qed.
  70
  71 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
  72 intro.elim i
  73   [rewrite < minus_n_O.
  74    simplify.rewrite < plus_n_O.
  75    apply le_n
  76   |simplify.
  77    apply (trans_le ? ((m)\sup(n)*(m-n)!))
  78     [apply H.
  79      apply lt_to_le.assumption
  80     |rewrite > sym_times in ⊢ (? ? (? % ?)).
  81      rewrite > assoc_times.
  82      apply le_times_r.
  83      generalize in match H1.
  84      cases m;intro
  85       [apply False_ind.
  86        apply (lt_to_not_le ? ? H2).
  87        apply le_O_n
  88       |rewrite > minus_Sn_m.
  89        simplify.
  90        apply le_plus_r.
  91        apply le_times_l.
  92        apply le_minus_m.
  93        apply le_S_S_to_le.
  94        assumption
  95       ]
  96     ]
  97   ]
  98 qed.
  99
 100 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
 101 intros.elim H
 102   [apply le_n
 103   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
 104    rewrite < assoc_times.
 105    rewrite < sym_times in ⊢ (? (? % ?) ?).
 106    rewrite > assoc_times.
 107    apply le_times_r.
 108    apply (trans_le ? (exp n1 n1))
 109     [assumption
 110     |apply monotonic_exp1.
 111      apply le_n_Sn
 112     ]
 113   ]
 114 qed.
 115
 116 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
 117 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 118 intro.
 119 rewrite > exp_S_sigma_p.
 120 apply le_sigma_p.
 121 intros.unfold bc.
 122 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 123   [rewrite > sym_times.
 124    apply le_times_r.
 125    rewrite > sym_times.
 126    rewrite < eq_div_div_div_times
 127     [apply monotonic_div
 128       [apply lt_O_fact
 129       |apply le_times_to_le_div2
 130         [apply lt_O_fact
 131         |apply le_fact_exp.
 132          apply le_S_S_to_le.
 133          assumption
 134         ]
 135       ]
 136     |apply lt_O_fact
 137     |apply lt_O_fact
 138     ]
 139   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 140     [rewrite > exp_plus_times.
 141      apply le_times_div_div_times.
 142      apply lt_O_fact
 143     |apply le_S_S_to_le.
 144      assumption
 145     ]
 146   ]
 147 qed.
 148
 149 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
 150 (exp (S n) n) <
 151 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 152 intros.
 153 rewrite > exp_S_sigma_p.
 154 apply lt_sigma_p
 155   [intros.unfold bc.
 156    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 157     [rewrite > sym_times.
 158      apply le_times_r.
 159      rewrite > sym_times.
 160      rewrite < eq_div_div_div_times
 161       [apply monotonic_div
 162         [apply lt_O_fact
 163         |apply le_times_to_le_div2
 164           [apply lt_O_fact
 165           |apply le_fact_exp.
 166            apply le_S_S_to_le.
 167            assumption
 168           ]
 169         ]
 170       |apply lt_O_fact
 171       |apply lt_O_fact
 172       ]
 173     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 174       [rewrite > exp_plus_times.
 175        apply le_times_div_div_times.
 176        apply lt_O_fact
 177       |apply le_S_S_to_le.
 178        assumption
 179       ]
 180     ]
 181   |apply (ex_intro ? ? n).
 182    split
 183     [split
 184       [apply le_n
 185       |reflexivity
 186       ]
 187     |rewrite < minus_n_n.
 188      rewrite > bc_n_n.
 189      simplify.unfold lt.
 190      apply le_times_to_le_div
 191       [apply lt_O_fact
 192       |rewrite > sym_times.
 193        apply le_fact_exp1.
 194        assumption
 195       ]
 196     ]
 197   ]
 198 qed.
 199
 200 theorem le_exp_SSO_fact:\forall n.
 201 exp (S(S O)) (pred n) \le n!.
 202 intro.elim n
 203   [apply le_n
 204   |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
 205    apply (nat_case1 n1);intros
 206     [apply le_n
 207     |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
 208      apply le_times
 209       [apply le_S_S.apply le_S_S.apply le_O_n
 210       |rewrite < H1.assumption
 211       ]
 212     ]
 213   ]
 214 qed.
 215
 216 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
 217 (exp (S n) n) < (S(S(S O)))*(exp n n).
 218 intros.
 219 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
 220   [apply lt_exp_sigma_p_exp.assumption
 221   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 222     [apply le_sigma_p.intros.
 223      apply le_times_to_le_div
 224       [apply lt_O_exp.
 225        apply lt_O_S
 226       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 227         [apply le_times_div_div_times.
 228          apply lt_O_fact
 229         |apply le_times_to_le_div2
 230           [apply lt_O_fact
 231           |rewrite < sym_times.
 232            apply le_times_r.
 233            apply le_exp_SSO_fact
 234           ]
 235         ]
 236       ]
 237     |rewrite > eq_sigma_p_pred
 238       [rewrite > div_SO.
 239        rewrite > sym_plus.
 240        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 241        apply le_plus_r.
 242        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)))
 243         [apply sigma_p_div_exp
 244         |apply le_times_to_le_div2
 245           [apply lt_O_exp.
 246            apply lt_O_S.
 247           |apply le_minus_m
 248           ]
 249         ]
 250       |reflexivity
 251       ]
 252     ]
 253   ]
 254 qed.
 255
 256 theorem lt_exp_Sn_n_SSSO: \forall n.
 257 (exp (S n) n) < (S(S(S O)))*(exp n n).
 258 intro.cases n;intros
 259   [simplify.apply le_S.apply le_n
 260   |cases n1;intros
 261     [simplify.apply le_n
 262     |apply lt_SO_to_lt_exp_Sn_n_SSSO.
 263      apply le_S_S.apply le_S_S.apply le_O_n
 264     ]
 265   ]
 266 qed.
 267
 268 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
 269 divides n m \to
 270 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
 271 intros.
 272 elim H1.rewrite > H2.
 273 rewrite < exp_exp_times.
 274 rewrite < exp_exp_times.
 275 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
 276 rewrite > lt_O_to_div_times
 277   [rewrite > times_exp.
 278    apply lt_exp1
 279     [apply (O_lt_times_to_O_lt ? n).
 280      rewrite > sym_times.
 281      rewrite < H2.
 282      assumption
 283     |apply lt_exp_Sn_n_SSSO
 284     ]
 285   |apply (O_lt_times_to_O_lt ? n2).
 286    rewrite < H2.
 287    assumption
 288   ]
 289 qed.
 290
 291 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
 292 divides n m \to
 293 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
 294 intros.
 295 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
 296   [apply le_log
 297     [assumption
 298     |apply lt_to_le.
 299      apply lt_exp_Sn_m_SSSO;assumption
 300     ]
 301   |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
 302     [apply log_times.
 303      assumption
 304     |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
 305      apply le_S_S.
 306      apply le_plus_l.
 307      apply log_exp1.
 308      assumption
 309     ]
 310   ]
 311 qed.
 312
 313 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
 314 O < a \to a \le b \to b \le n \to
 315 log p (exp b n!) - log p (exp a n!) \le
 316 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
 317 intros 7.
 318 elim b
 319   [simplify.
 320    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
 321    apply le_n.
 322   |apply (bool_elim ? (leb a n1));intro
 323     [rewrite > true_to_sigma_p_Sn
 324       [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
 325         [rewrite > sym_plus.
 326          rewrite > plus_minus
 327           [apply le_plus_to_minus_r.
 328            rewrite < plus_minus_m_m
 329             [rewrite > sym_plus.
 330              apply le_log_exp_Sn_log_exp_n
 331               [apply lt_O_fact
 332               |assumption
 333               |apply divides_fact;
 334                  [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
 335                  |apply lt_to_le;assumption]]
 336             |apply le_log
 337               [assumption
 338               |cut (O = exp O n!)
 339                  [rewrite > Hcut;apply monotonic_exp1;constructor 2;
 340                   apply leb_true_to_le;assumption
 341                  |elim n
 342                     [reflexivity
 343                     |simplify;rewrite > exp_plus_times;rewrite < H6;
 344                      rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
 345         |apply le_log
 346           [assumption
 347           |apply monotonic_exp1;apply leb_true_to_le;assumption]]
 348       |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
 349        rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
 350     |assumption]
 351   |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
 352    rewrite > eq_minus_n_m_O
 353     [apply le_O_n
 354     |apply le_log
 355        [assumption
 356        |apply monotonic_exp1;assumption]]]]
 357 qed.
 358
 359 theorem le_exp_div:\forall n,m,q. O < m \to
 360 exp (n/m) q \le (exp n q)/(exp m q).
 361 intros.
 362 apply le_times_to_le_div
 363   [apply lt_O_exp.
 364    assumption
 365   |rewrite > times_exp.
 366    rewrite < sym_times.
 367    apply monotonic_exp1.
 368    rewrite > (div_mod n m) in ⊢ (? ? %)
 369     [apply le_plus_n_r
 370     |assumption
 371     ]
 372   ]
 373 qed.
 374
 375 theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
 376 O < a \to a \le b \to b \le n \to
 377 log p (b/a) \le
 378 (sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
 379 intros.
 380 apply le_times_to_le_div
 381   [apply lt_O_fact
 382   |apply (trans_le ? (log p (exp (b/a) n!)))
 383     [apply log_exp2
 384       [assumption
 385       |apply le_times_to_le_div
 386         [assumption
 387         |rewrite < times_n_SO.
 388          assumption
 389         ]
 390       ]
 391     |apply (trans_le ? (log p ((exp b n!)/(exp a n!))))
 392       [apply le_log
 393         [assumption
 394         |apply le_exp_div.assumption
 395         ]
 396       |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
 397         [apply log_div
 398           [assumption
 399           |apply lt_O_exp.
 400            assumption
 401           |apply monotonic_exp1.
 402            assumption
 403           ]
 404         |apply le_log_exp_fact_sigma_p;assumption
 405         ]
 406       ]
 407     ]
 408   ]
 409 qed.
 410
 411 theorem sigma_p_log_div1: \forall n,b. S O < b \to
 412 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 413 \le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 414 ).
 415 intros.
 416 apply le_sigma_p.intros.
 417 apply le_log_div_sigma_p
 418   [assumption
 419   |apply prime_to_lt_O.
 420    apply primeb_true_to_prime.
 421    apply (andb_true_true ? ? H2)
 422   |apply le_S_S_to_le.
 423    assumption
 424   |apply le_n
 425   ]
 426 qed.
 427
 428 theorem sigma_p_log_div2: \forall n,b. S O < b \to
 429 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 430 \le
 431 (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!).
 432 intros.
 433 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 434 )))
 435   [apply sigma_p_log_div1.assumption
 436   |apply le_times_to_le_div
 437     [apply lt_O_fact
 438     |rewrite > distributive_times_plus_sigma_p.
 439      rewrite < sym_times in ⊢ (? ? %).
 440      rewrite > distributive_times_plus_sigma_p.
 441      apply le_sigma_p.intros.
 442      apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!)))
 443       [apply le_times_div_div_times.
 444        apply lt_O_fact
 445       |rewrite > sym_times.
 446        rewrite > lt_O_to_div_times
 447         [rewrite > distributive_times_plus_sigma_p.
 448          apply le_sigma_p.intros.
 449          rewrite < times_n_Sm in ⊢ (? ? %).
 450          rewrite > plus_n_SO.
 451          rewrite > sym_plus.
 452          apply le_plus
 453           [apply le_S_S.apply le_O_n
 454           |rewrite < sym_times.
 455            apply le_n
 456           ]
 457         |apply lt_O_fact
 458         ]
 459       ]
 460     ]
 461   ]
 462 qed.
 463
 464 theorem sigma_p_log_div: \forall n,b. S O < b \to
 465 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 466 \le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n!
 467 .
 468 intros.
 469 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!))
 470   [apply sigma_p_log_div2.assumption
 471   |apply monotonic_div
 472     [apply lt_O_fact
 473     |apply le_times_l.
 474      unfold prim.
 475      cut
 476      (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p))
 477       (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i)))
 478      = sigma_p n (λi:nat.leb (S n) (i*i))
 479        (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))))
 480       [rewrite > Hcut.
 481        apply le_sigma_p.intros.
 482        rewrite < sym_times.
 483        rewrite > distributive_times_plus_sigma_p.
 484        rewrite < times_n_SO.
 485        cut
 486         (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))
 487          = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))
 488         [rewrite > Hcut1.
 489          apply le_sigma_p1.intros.
 490          rewrite < andb_sym.
 491          rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?).
 492          apply (bool_elim  ? (leb i1 i));intros
 493           [apply (bool_elim  ? (leb (S n) (i1*i1)));intros
 494             [apply le_n
 495             |apply le_O_n
 496             ]
 497           |apply le_O_n
 498           ]
 499         |apply or_false_to_eq_sigma_p
 500           [apply le_S.assumption
 501           |intros.
 502            left.rewrite > (lt_to_leb_false i1 i)
 503             [rewrite > andb_sym.reflexivity
 504             |assumption
 505             ]
 506           ]
 507         ]
 508       |apply sigma_p_sigma_p.intros.
 509        apply (bool_elim ? (leb x y));intros
 510         [apply (bool_elim ? (leb (S n) (x*x)));intros
 511           [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?))
 512             [reflexivity
 513             |apply (trans_le ? (x*x))
 514               [apply leb_true_to_le.assumption
 515               |apply le_times;apply leb_true_to_le;assumption
 516               ]
 517             ]
 518           |rewrite < andb_sym in ⊢ (? ? (? % ?) ?).
 519            rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))).
 520            rewrite < andb_sym in ⊢ (? ? ? %).
 521            reflexivity
 522           ]
 523         |rewrite < andb_sym.
 524          rewrite > andb_assoc in ⊢ (? ? ? %).
 525          rewrite < andb_sym in ⊢ (? ? ? (? % ?)).
 526          reflexivity
 527         ]
 528       ]
 529     ]
 530   ]
 531 qed.
 532
 533 theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to
 534 sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i))
 535 \leq ((S (S O)) * n * m)/(pred (log b n)).
 536 intros.
 537 apply (trans_le ? (sigma_p (S n)
 538              (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n)))))
 539   [apply le_sigma_p;intros;apply le_times_to_le_div
 540      [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
 541       apply le_plus_to_minus_r;simplify;
 542       rewrite < (eq_log_exp b ? H);
 543       apply le_log;
 544           [assumption
 545           |simplify;rewrite < times_n_SO;assumption]
 546      |apply (trans_le ? ((pred (log b n) * m)/log b i))
 547         [apply le_times_div_div_times;apply lt_O_log
 548           [elim (le_to_or_lt_eq ? ? (le_O_n i))
 549             [assumption
 550             |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
 551              reflexivity]
 552           |apply (le_exp_to_le1 ? ? (S (S O)))
 553             [apply lt_O_S;
 554             |apply (trans_le ? (S n))
 555                [apply le_S;simplify;rewrite < times_n_SO;assumption
 556                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
 557         |apply le_times_to_le_div2
 558           [apply lt_O_log
 559             [elim (le_to_or_lt_eq ? ? (le_O_n i))
 560               [assumption
 561               |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
 562                reflexivity]
 563           |apply (le_exp_to_le1 ? ? (S (S O)))
 564             [apply lt_O_S;
 565             |apply (trans_le ? (S n))
 566                [apply le_S;simplify;rewrite < times_n_SO;assumption
 567                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
 568           |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times;
 569            apply le_times_l;rewrite > sym_times;
 570            rewrite > minus_n_O in \vdash (? (? %) ?);
 571            rewrite < eq_minus_S_pred;apply le_plus_to_minus;
 572            simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i)))
 573              [apply le_log
 574                 [assumption
 575                 |apply lt_to_le;apply leb_true_to_le;assumption]
 576              |rewrite > sym_plus;simplify;apply log_times;assumption]]]]
 577         |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?);
 578          rewrite < distributive_times_plus_sigma_p;
 579          apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n))
 580            [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)))
 581              [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO;
 582               apply (bool_elim ? (leb (S n) (i*i)))
 583                 [intro;cut (leb (S O) (i*i) = true)
 584                   [rewrite > Hcut;apply le_n
 585                   |apply le_to_leb_true;apply (trans_le ? (S n))
 586                      [apply le_S_S;apply le_O_n
 587                      |apply leb_true_to_le;assumption]]
 588                 |intro;simplify in \vdash (? % ?);apply le_O_n]
 589              |elim n
 590                 [simplify;apply le_n
 591                 |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro
 592                    [rewrite > true_to_sigma_p_Sn
 593                       [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)));
 594                        apply le_S_S;assumption
 595                       |assumption]
 596                    |rewrite > false_to_sigma_p_Sn
 597                       [apply le_S;assumption
 598                       |assumption]]]]
 599           |rewrite > sym_times in \vdash (? % ?);
 600            rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
 601            rewrite > assoc_times;
 602            apply le_times_div_div_times;
 603            rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
 604            apply le_plus_to_minus_r;simplify;
 605            rewrite < (eq_log_exp b ? H);
 606            apply le_log;
 607              [assumption
 608              |simplify;rewrite < times_n_SO;assumption]]]
 609 qed.
 610
 611 lemma neper_sigma_p1 : \forall n,a.n \divides a \to
 612 exp (a * S n) n =
 613 sigma_p (S n) (\lambda x.true) (\lambda k.(bc n k)*(exp n (n-k))*(exp a n)).
 614 intros;rewrite < times_exp;rewrite > exp_S_sigma_p;
 615 rewrite > distributive_times_plus_sigma_p;
 616 apply eq_sigma_p;intros;
 617   [reflexivity
 618   |rewrite > sym_times;reflexivity;]
 619 qed.
 620
 621 lemma eq_exp_pi_p : \forall a,n.(exp a n) = pi_p n (\lambda x.true) (\lambda x.a).
 622 intros;elim n
 623   [simplify;reflexivity
 624   |change in \vdash (? ? % ?) with (a*exp a n1);rewrite > true_to_pi_p_Sn
 625      [apply eq_f2
 626         [reflexivity
 627         |assumption]
 628      |reflexivity]]
 629 qed.
 630
 631 lemma eq_fact_pi_p : \forall n.n! = pi_p n (\lambda x.true) (\lambda x.S x).
 632 intros;elim n
 633   [simplify;reflexivity
 634   |rewrite > true_to_pi_p_Sn
 635      [change in \vdash (? ? % ?) with (S n1*n1!);apply eq_f2
 636         [reflexivity
 637         |assumption]
 638      |reflexivity]]
 639 qed.
 640
 641 lemma divides_pi_p : \forall m,n,p,f.m \leq n \to pi_p m p f \divides pi_p n p f.
 642 intros;elim H
 643   [apply divides_n_n
 644   |apply (bool_elim ? (p n1));intro
 645      [rewrite > true_to_pi_p_Sn
 646         [rewrite > sym_times;rewrite > times_n_SO;apply divides_times
 647            [assumption
 648            |apply divides_SO_n]
 649         |assumption]
 650      |rewrite > false_to_pi_p_Sn;assumption]]
 651 qed.
 652
 653 lemma divides_fact_fact : \forall m,n.m \leq n \to m! \divides n!.
 654 intros;do 2 rewrite > eq_fact_pi_p;apply divides_pi_p;assumption.
 655 qed.
 656
 657 lemma divides_times_to_eq : \forall a,b,c.O < c \to c \divides a \to a*b/c = a/c*b.
 658 intros;elim H1;rewrite > H2;cases H;rewrite > assoc_times;do 2 rewrite > div_times;
 659 reflexivity;
 660 qed.
 661
 662 lemma divides_pi_p_to_eq : \forall k,p,f,g.(\forall x.p x = true \to O < g x \land (g x \divides f x)) \to
 663 pi_p k p f/pi_p k p g = pi_p k p (\lambda x.(f x)/(g x)).
 664 intros;
 665 cut (\forall k1.(pi_p k1 p g \divides pi_p k1 p f))
 666   [|intro;elim k1
 667      [simplify;apply divides_n_n
 668      |apply (bool_elim ? (p n));intro;
 669         [rewrite > true_to_pi_p_Sn
 670            [rewrite > true_to_pi_p_Sn
 671               [elim (H n)
 672                  [elim H4;elim H1;rewrite > H5;rewrite > H6;
 673                   rewrite < assoc_times;rewrite > assoc_times in ⊢ (? ? (? % ?));
 674                   rewrite > sym_times in ⊢ (? ? (? (? ? %) ?));
 675                   rewrite > assoc_times;rewrite > assoc_times;
 676                   apply divides_times
 677                     [apply divides_n_n
 678                     |rewrite > times_n_SO in \vdash (? % ?);apply divides_times
 679                        [apply divides_n_n
 680                        |apply divides_SO_n]]
 681                  |assumption]
 682               |assumption]
 683            |assumption]
 684         |rewrite > false_to_pi_p_Sn
 685            [rewrite > false_to_pi_p_Sn
 686               [assumption
 687               |assumption]
 688            |assumption]]]]
 689 elim k
 690   [simplify;reflexivity
 691   |apply (bool_elim ? (p n))
 692      [intro;rewrite > true_to_pi_p_Sn;
 693         [rewrite > true_to_pi_p_Sn;
 694            [rewrite > true_to_pi_p_Sn;
 695               [elim (H n);
 696                  [elim H4;rewrite > H5;rewrite < eq_div_div_div_times;
 697                     [cases H3
 698                        [rewrite > assoc_times;do 2 rewrite > div_times;
 699                         elim (Hcut n);rewrite > H6;rewrite < assoc_times;
 700                         rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?);
 701                         cut (O < pi_p n p g)
 702                           [rewrite < H1;rewrite > H6;cases Hcut1;
 703                            rewrite > assoc_times;do 2 rewrite > div_times;reflexivity
 704                           |elim n
 705                              [simplify;apply le_n
 706                              |apply (bool_elim ? (p n3));intro
 707                                 [rewrite > true_to_pi_p_Sn
 708                                    [rewrite > (times_n_O O);apply lt_times
 709                                       [elim (H n3);assumption
 710                                       |assumption]
 711                                    |assumption]
 712                                 |rewrite > false_to_pi_p_Sn;assumption]]]
 713                        |rewrite > assoc_times;do 2 rewrite > div_times;
 714                         elim (Hcut n);rewrite > H7;rewrite < assoc_times;
 715                         rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?);
 716                         cut (O < pi_p n p g)
 717                           [rewrite < H1;rewrite > H7;cases Hcut1;
 718                            rewrite > assoc_times;do 2 rewrite > div_times;reflexivity
 719                           |elim n
 720                              [simplify;apply le_n
 721                              |apply (bool_elim ? (p n3));intro
 722                                 [rewrite > true_to_pi_p_Sn
 723                                    [rewrite > (times_n_O O);apply lt_times
 724                                       [elim (H n3);assumption
 725                                       |assumption]
 726                                    |assumption]
 727                                 |rewrite > false_to_pi_p_Sn;assumption]]]]
 728                     |assumption
 729                     |(*già usata 2 volte: fattorizzare*)
 730                      elim n
 731                        [simplify;apply le_n
 732                        |apply (bool_elim ? (p n1));intro
 733                           [rewrite > true_to_pi_p_Sn
 734                              [rewrite > (times_n_O O);apply lt_times
 735                                 [elim (H n1);assumption
 736                                 |assumption]
 737                              |assumption]
 738                           |rewrite > false_to_pi_p_Sn;assumption]]]
 739                  |assumption]
 740               |assumption]
 741            |assumption]
 742         |assumption]
 743      |intro;rewrite > (false_to_pi_p_Sn ? ? ? H2);
 744       rewrite > (false_to_pi_p_Sn ? ? ? H2);rewrite > (false_to_pi_p_Sn ? ? ? H2);
 745       assumption]]
 746 qed.
 747
 748 lemma divides_times_to_divides_div : \forall a,b,c.O < b \to
 749                                     a*b \divides c \to a \divides c/b.
 750 intros;elim H1;rewrite > H2;rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
 751 rewrite > assoc_times;cases H;rewrite > div_times;rewrite > times_n_SO in \vdash (? % ?);
 752 apply divides_times
 753   [1,3:apply divides_n_n
 754   |*:apply divides_SO_n]
 755 qed.
 756
 757 lemma neper_sigma_p2 : \forall n,a.O < n \to n \divides a \to
 758 sigma_p (S n) (\lambda x.true) (\lambda k.((bc n k)*(exp a n)*(exp n (n-k)))/(exp n n))
 759 = sigma_p (S n) (\lambda x.true)
 760 (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!).
 761 intros;apply eq_sigma_p;intros;
 762   [reflexivity
 763   |transitivity (bc n x*exp a n/exp n x)
 764      [rewrite > minus_n_O in ⊢ (? ? (? ? (? ? %)) ?);
 765       rewrite > (minus_n_n x);
 766       rewrite < (eq_plus_minus_minus_minus n x x);
 767         [rewrite > exp_plus_times;
 768          rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
 769          rewrite < eq_div_div_times;
 770            [reflexivity
 771            |*:apply lt_O_exp;assumption]
 772         |apply le_n
 773         |apply le_S_S_to_le;assumption]
 774      |rewrite > minus_n_O in ⊢ (? ? (? (? ? (? ? %)) ?) ?);
 775       rewrite > (minus_n_n x);
 776       rewrite < (eq_plus_minus_minus_minus n x x);
 777         [rewrite > exp_plus_times;
 778          unfold bc;
 779          elim (bc2 n x)
 780            [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
 781               [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
 782                rewrite > assoc_times;rewrite > sym_times in ⊢ (? ? (? (? (? ? %) ?) ?) ?);
 783                rewrite < eq_div_div_times
 784                  [rewrite > Hcut;rewrite < assoc_times;
 785                   cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x)
 786                     = pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!)
 787                     [rewrite > Hcut1;rewrite < times_pi_p;
 788                      rewrite > divides_times_to_eq in \vdash (? ? % ?);
 789                        [rewrite > eq_div_div_div_times;
 790                           [rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
 791                            rewrite < eq_div_div_div_times;
 792                              [cut (exp n x = pi_p x (\lambda i.true) (\lambda i.n))
 793                                 [rewrite > Hcut2;rewrite > divides_pi_p_to_eq
 794                                    [rewrite > sym_times in \vdash (? ? ? %);
 795                                     rewrite > divides_times_to_eq in \vdash (? ? ? %);
 796                                       [apply eq_f2
 797                                          [apply eq_f2
 798                                             [apply eq_pi_p;intros
 799                                                [reflexivity
 800                                                |rewrite > sym_times;
 801                                                 rewrite > distr_times_minus;elim H1;
 802                                                 rewrite > H5;(* in ⊢ (? ? (? (? ? (? % ?)) ?) ?);*)
 803                                                 rewrite > sym_times;rewrite > assoc_times;
 804                                                 rewrite < distr_times_minus;
 805                                                 generalize in match H;cases n;intros
 806                                                   [elim (not_le_Sn_O ? H6)
 807                                                   |do 2 rewrite > div_times;reflexivity]]
 808                                             |reflexivity]
 809                                          |reflexivity]
 810                                       |apply lt_O_fact
 811                                       |cut (pi_p x (λy:nat.true) (λi:nat.a-a*i/n) = (exp a x)/(exp n x)*(n!/(n-x)!))
 812                                          [rewrite > Hcut3;rewrite > times_n_SO;
 813                                           rewrite > sym_times;apply divides_times
 814                                             [apply divides_SO_n;
 815                                             |apply divides_times_to_divides_div;
 816                                                [apply lt_O_fact
 817                                                |apply bc2;apply le_S_S_to_le;assumption]]
 818                                          |cut (pi_p x (\lambda y.true) (\lambda i. a - a*i/n) =
 819                                               pi_p x (\lambda y.true) (\lambda i. a*(n-i)/n))
 820                                             [rewrite > Hcut3;
 821                                              rewrite < (divides_pi_p_to_eq ? ? (\lambda i.(a*(n-i))) (\lambda i.n))
 822                                                [rewrite > (times_pi_p ? ? (\lambda i.a) (\lambda i.(n-i)));
 823                                                 rewrite > divides_times_to_eq;
 824                                                   [apply eq_f2
 825                                                      [apply eq_f2;rewrite < eq_exp_pi_p;reflexivity
 826                                                      |rewrite < Hcut;rewrite > H3;
 827                                                       rewrite < sym_times in ⊢ (? ? ? (? (? % ?) ?));
 828                                                       rewrite > (S_pred ((n-x)!));
 829                                                         [rewrite > assoc_times;
 830                                                          rewrite > div_times;reflexivity
 831                                                         |apply lt_O_fact]]
 832                                                   |unfold lt;cut (1 = pi_p x (\lambda y.true) (\lambda y.1))
 833                                                      [rewrite > Hcut4;apply le_pi_p;intros;assumption
 834                                                      |elim x
 835                                                         [simplify;reflexivity
 836                                                         |rewrite > true_to_pi_p_Sn;
 837                                                            [rewrite < H4;reflexivity
 838                                                            |reflexivity]]]
 839                                                   |elim x
 840                                                      [simplify;apply divides_SO_n
 841                                                      |rewrite > true_to_pi_p_Sn
 842                                                         [rewrite > true_to_pi_p_Sn
 843                                                            [apply divides_times;assumption
 844                                                            |reflexivity]
 845                                                         |reflexivity]]]
 846                                                |intros;split
 847                                                   [assumption
 848                                                   |rewrite > times_n_SO;apply divides_times
 849                                                      [assumption
 850                                                      |apply divides_SO_n]]]
 851                                             |apply eq_pi_p;intros;
 852                                                [reflexivity
 853                                                |elim H1;rewrite > H5;rewrite > (S_pred n);
 854                                                   [rewrite > assoc_times;
 855                                                    rewrite > assoc_times;
 856                                                    rewrite > div_times;
 857                                                    rewrite > div_times;
 858                                                    rewrite > distr_times_minus;
 859                                                    rewrite > sym_times;
 860                                                    reflexivity
 861                                                   |assumption]]]]]
 862                                    |intros;split
 863                                       [assumption
 864                                       |rewrite > sym_times;rewrite > times_n_SO;
 865                                        apply divides_times
 866                                          [assumption
 867                                          |apply divides_SO_n]]]
 868                                 |rewrite < eq_exp_pi_p;reflexivity]
 869                              |apply lt_O_exp;assumption
 870                              |apply lt_O_fact]
 871                           |apply lt_O_fact
 872                           |apply lt_O_exp;assumption]
 873                        |apply lt_O_exp;assumption
 874                        |rewrite > (times_pi_p ? ? (\lambda x.(n-x)) (\lambda x.a));
 875                         rewrite > divides_times_to_eq
 876                           [rewrite > times_n_SO;rewrite > sym_times;apply divides_times
 877                              [apply divides_SO_n
 878                              |elim x
 879                                 [simplify;apply divides_SO_n
 880                                 |change in \vdash (? % ?) with (n*(exp n n1));
 881                                  rewrite > true_to_pi_p_Sn
 882                                    [apply divides_times;assumption
 883                                    |reflexivity]]]
 884                           |apply lt_O_fact
 885                           |apply (witness ? ? n2);symmetry;assumption]]
 886                     |rewrite > divides_times_to_eq;
 887                        [apply eq_f2
 888                           [reflexivity
 889                           |elim x
 890                              [simplify;reflexivity
 891                              |change in \vdash (? ? % ?) with (a*(exp a n1));
 892                               rewrite > true_to_pi_p_Sn
 893                                 [apply eq_f2
 894                                    [reflexivity
 895                                    |assumption]
 896                                 |reflexivity]]]
 897                        |apply lt_O_fact
 898                        |apply (witness ? ? n2);symmetry;assumption]]
 899                  |apply lt_O_fact
 900                  |apply lt_O_fact]
 901               |apply (inj_times_r (pred ((n-x)!)));
 902                rewrite < (S_pred ((n-x)!))
 903                  [rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
 904                   rewrite < H3;generalize in match H2;elim x
 905                     [rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
 906                     |rewrite < fact_minus in H4;
 907                        [rewrite > true_to_pi_p_Sn
 908                           [rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? (? % ?));
 909                            apply H4;apply lt_to_le;assumption
 910                           |reflexivity]
 911                        |apply le_S_S_to_le;assumption]]
 912                  |apply lt_O_fact]]
 913            |apply le_S_S_to_le;assumption]
 914         |apply le_n
 915         |apply le_S_S_to_le;assumption]]]
 916 qed.
 917
 918 lemma divides_sigma_p_to_eq : \forall k,p,f,b.O < b \to
 919  (\forall x.p x = true \to b \divides f x) \to
 920  (sigma_p k p f)/b = sigma_p k p (\lambda x. (f x)/b).
 921 intros;cut (\forall k1.b \divides sigma_p k1 p f)
 922   [|intro;elim k1
 923      [simplify;apply (witness ? ? O);rewrite < times_n_O;reflexivity
 924      |apply (bool_elim ? (p n));intro
 925         [rewrite > true_to_sigma_p_Sn;
 926            [elim (H1 n);
 927               [elim H2;rewrite > H4;rewrite > H5;rewrite < distr_times_plus;
 928                rewrite > times_n_SO in \vdash (? % ?);apply divides_times
 929                  [apply divides_n_n
 930                  |apply divides_SO_n]
 931               |assumption]
 932            |assumption]
 933         |rewrite > false_to_sigma_p_Sn;assumption]]]
 934 elim k
 935   [cases H;simplify;reflexivity
 936   |apply (bool_elim ? (p n));intro
 937      [rewrite > true_to_sigma_p_Sn
 938         [rewrite > true_to_sigma_p_Sn
 939            [elim (H1 n);
 940               [elim (Hcut n);rewrite > H4;rewrite > H5;rewrite < distr_times_plus;
 941                rewrite < H2;rewrite > H5;cases H;do 3 rewrite > div_times;
 942                reflexivity
 943               |assumption]
 944            |assumption]
 945         |assumption]
 946      |do 2 rewrite > false_to_sigma_p_Sn;assumption]]
 947 qed.
 948
 949 lemma neper_sigma_p3 : \forall a,n.O < a \to O < n \to n \divides a \to (exp (S n) n)/(exp n n) =
 950 sigma_p (S n) (\lambda x.true)
 951 (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n).
 952 intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
 953   [rewrite > eq_div_div_div_times
 954      [rewrite > sym_times in \vdash (? ? ? (? ? %));rewrite < eq_div_div_times;
 955         [reflexivity
 956         |apply lt_O_exp;assumption
 957         |apply lt_O_exp;assumption]
 958      |apply lt_O_exp;assumption
 959      |apply lt_O_exp;assumption]
 960   |apply eq_f2;
 961      [rewrite > times_exp;rewrite > neper_sigma_p1
 962         [transitivity (sigma_p (S n) (λx:nat.true) (λk:nat.bc n k*(a)\sup(n)*(exp n (n-k))/(exp n n)))
 963            [elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
 964             rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
 965             transitivity (sigma_p (S n) (λx:nat.true)
 966 (λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n2)\sup(n)))/exp n n)
 967               [apply eq_f2
 968                  [apply eq_sigma_p;intros;
 969                     [reflexivity
 970                     |rewrite < assoc_times;rewrite > sym_times;reflexivity]
 971                  |reflexivity]
 972               |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n2 n)));
 973                transitivity (sigma_p (S n) (λx:nat.true)
 974                 (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k)))
 975                  [rewrite > (S_pred (exp n n))
 976                     [rewrite > div_times;apply eq_sigma_p;intros
 977                        [reflexivity
 978                        |rewrite > sym_times;rewrite > sym_times in ⊢ (? ? ? (? % ?));
 979                         rewrite > assoc_times in \vdash (? ? ? %);reflexivity]
 980                     |apply lt_O_exp;assumption]
 981                  |apply eq_sigma_p;intros
 982                     [reflexivity
 983                     |rewrite < assoc_times;rewrite > assoc_times in \vdash (? ? ? %);
 984                      rewrite > sym_times in \vdash (? ? ? (? (? ? %) ?));
 985                      rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? %);
 986                      rewrite > (S_pred (exp n n))
 987                        [rewrite > div_times;reflexivity
 988                        |apply lt_O_exp;assumption]]]]
 989            |rewrite > neper_sigma_p2;
 990               [reflexivity
 991               |assumption
 992               |assumption]]
 993         |assumption]
 994      |reflexivity]]
 995 qed.
 996
 997 theorem neper_monotonic : \forall n. O < n \to
 998 (exp (S n) n)/(exp n n) \leq (exp (S (S n)) (S n))/(exp (S n) (S n)).
 999 intros;rewrite > (neper_sigma_p3 (n*S n) n)
1000   [rewrite > (neper_sigma_p3 (n*S n) (S n))
1001      [change in ⊢ (? ? (? ? %)) with ((n * S n)*(exp (n * S n) n));
1002       rewrite < eq_div_div_div_times
1003         [apply monotonic_div;
1004            [apply lt_O_exp;rewrite > (times_n_O O);apply lt_times
1005               [assumption
1006               |apply lt_O_S]
1007            |apply le_times_to_le_div
1008               [rewrite > (times_n_O O);apply lt_times
1009                  [assumption
1010                  |apply lt_O_S]
1011               |rewrite > distributive_times_plus_sigma_p;
1012                apply (trans_le ? (sigma_p (S n) (λx:nat.true)
1013                  (λk:nat.((n*S n))\sup(S n-k)*pi_p k (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n)/k!)))
1014                  [apply le_sigma_p;intros;rewrite > sym_times in ⊢ (? (? ? %) ?);
1015                   rewrite > sym_times in \vdash (? ? (? % ?));
1016                   rewrite > divides_times_to_eq in \vdash (? ? %)
1017                     [rewrite > divides_times_to_eq in \vdash (? % ?)
1018                        [rewrite > sym_times in \vdash (? (? ? %) ?);
1019                         rewrite < assoc_times;
1020                         rewrite > sym_times in \vdash (? ? %);
1021                         rewrite > minus_Sn_m;
1022                           [apply le_times_r;apply monotonic_div
1023                              [apply lt_O_fact
1024                              |apply le_pi_p;intros;apply monotonic_le_minus_r;
1025                               rewrite > assoc_times in \vdash (? % ?);
1026                               rewrite > sym_times in \vdash (? % ?);
1027                               rewrite > assoc_times in \vdash (? % ?);
1028                               rewrite > div_times;
1029                               rewrite > (S_pred n) in \vdash (? ? %);
1030                                 [rewrite > assoc_times;rewrite > div_times;
1031                                  rewrite < S_pred
1032                                    [rewrite > sym_times;apply le_times_l;apply le_S;apply le_n
1033                                    |assumption]
1034                                 |assumption]]
1035                           |apply le_S_S_to_le;assumption]
1036                        |apply lt_O_fact
1037                        |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/n) =
1038                              pi_p i (\lambda y.true) (\lambda i.S n) *
1039                              pi_p i (\lambda y.true) (\lambda i.(n-i)))
1040                           [rewrite > Hcut;rewrite > times_n_SO;
1041                            rewrite > sym_times;apply divides_times
1042                              [apply divides_SO_n
1043                              |elim (bc2 n i);
1044                                 [apply (witness ? ? n2);
1045                                  cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
1046                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
1047                                     rewrite > (S_pred ((n-i)!))
1048                                       [rewrite > assoc_times;rewrite > div_times;
1049                                        reflexivity
1050                                       |apply lt_O_fact]
1051                                    |generalize in match H1;elim i
1052                                       [rewrite < minus_n_O;rewrite > div_n_n;
1053                                          [reflexivity
1054                                          |apply lt_O_fact]
1055                                       |rewrite > true_to_pi_p_Sn
1056                                          [rewrite > H4
1057                                             [rewrite > sym_times;rewrite < divides_times_to_eq
1058                                                [rewrite < fact_minus
1059                                                   [rewrite > sym_times;
1060                                                    rewrite < eq_div_div_times
1061                                                      [reflexivity
1062                                                      |apply lt_to_lt_O_minus;apply le_S_S_to_le;
1063                                                       assumption
1064                                                      |apply lt_O_fact;]
1065                                                   |apply le_S_S_to_le;assumption]
1066                                                |apply lt_O_fact
1067                                                |apply divides_fact_fact;
1068                                                 apply le_plus_to_minus;
1069                                                 rewrite > plus_n_O in \vdash (? % ?);
1070                                                 apply le_plus_r;apply le_O_n]
1071                                             |apply lt_to_le;assumption]
1072                                          |reflexivity]]]
1073                                 |apply le_S_S_to_le;assumption]]
1074                           |rewrite < times_pi_p;apply eq_pi_p;intros;
1075                              [reflexivity
1076                              |rewrite > distr_times_minus;rewrite > assoc_times;
1077                               rewrite > (S_pred n) in \vdash (? ? (? ? (? (? % ?) %)) ?)
1078                                 [rewrite > div_times;rewrite > sym_times;reflexivity
1079                                 |assumption]]]]
1080                     |apply lt_O_fact
1081                     |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n) =
1082                              pi_p i (\lambda y.true) (\lambda i.n) *
1083                              pi_p i (\lambda y.true) (\lambda i.(S n-i)))
1084                           [rewrite > Hcut;rewrite > times_n_SO;rewrite > sym_times;
1085                            apply divides_times
1086                              [apply divides_SO_n
1087                              |elim (bc2 (S n) i);
1088                                 [apply (witness ? ? n2);
1089                                  cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
1090                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
1091                                     rewrite > (S_pred ((S n-i)!))
1092                                       [rewrite > assoc_times;rewrite > div_times;
1093                                        reflexivity
1094                                       |apply lt_O_fact]
1095                                    |generalize in match H1;elim i
1096                                       [rewrite < minus_n_O;rewrite > div_n_n;
1097                                          [reflexivity
1098                                          |apply lt_O_fact]
1099                                       |rewrite > true_to_pi_p_Sn
1100                                          [rewrite > H4
1101                                             [rewrite > sym_times;rewrite < divides_times_to_eq
1102                                                [rewrite < fact_minus
1103                                                   [rewrite > sym_times;
1104                                                    rewrite < eq_div_div_times
1105                                                      [reflexivity
1106                                                      |apply lt_to_lt_O_minus;apply lt_to_le;
1107                                                       assumption
1108                                                      |apply lt_O_fact]
1109                                                   |apply lt_to_le;assumption]
1110                                                |apply lt_O_fact
1111                                                |apply divides_fact_fact;
1112                                                 apply le_plus_to_minus;
1113                                                 rewrite > plus_n_O in \vdash (? % ?);
1114                                                 apply le_plus_r;apply le_O_n]
1115                                             |apply lt_to_le;assumption]
1116                                          |reflexivity]]]
1117                                 |apply lt_to_le;assumption]]
1118                           |rewrite < times_pi_p;apply eq_pi_p;intros;
1119                              [reflexivity
1120                              |rewrite > distr_times_minus;rewrite > sym_times in \vdash (? ? (? ? (? (? % ?) ?)) ?);
1121                               rewrite > assoc_times;rewrite > div_times;reflexivity]]]
1122                     |rewrite > true_to_sigma_p_Sn in \vdash (? ? %)
1123                        [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
1124                         apply le_plus_r;apply le_O_n
1125                        |reflexivity]]]]
1126            |rewrite > (times_n_O O);apply lt_times
1127               [assumption
1128               |apply lt_O_S]
1129            |apply lt_O_exp;rewrite > (times_n_O O);apply lt_times
1130               [assumption
1131               |apply lt_O_S]]
1132         |rewrite > (times_n_O O);apply lt_times
1133            [assumption
1134            |apply lt_O_S]
1135         |apply lt_O_S
1136         |apply (witness ? ? n);apply sym_times]
1137      |rewrite > (times_n_O O);apply lt_times
1138         [assumption
1139         |apply lt_O_S]
1140      |assumption
1141      |apply (witness ? ? (S n));reflexivity]
1142 qed.
1143
1144 theorem le_SSO_neper : \forall n.O < n \to (2 \leq (exp (S n) n)/(exp n n)).
1145 intros;elim H
1146   [simplify;apply le_n
1147   |apply (trans_le ? ? ? H2);apply neper_monotonic;assumption]
1148 qed.
1149
1150 theorem le_SSO_exp_neper : \forall n.O < n \to 2*(exp n n) \leq exp (S n) n.
1151 intros;apply (trans_le ? ((exp (S n) n)/(exp n n)*(exp n n)))
1152   [apply le_times_l;apply le_SSO_neper;assumption
1153   |rewrite > sym_times;apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?))
1154      [apply lt_O_exp;assumption
1155      |cases (lt_O_exp ? n H);rewrite > div_times;apply le_n]]
1156 qed.
1157
1158 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
1159 divides n m \to
1160 log p (exp n m) - log p (exp a m) \le
1161 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
1162 intros.
1163 elim n
1164   [rewrite > false_to_sigma_p_Sn.
1165    simplify.
1166    apply (lt_O_n_elim ? H).intro.
1167    simplify.apply le_O_n
1168   |apply (bool_elim ? (leb a n1));intro
1169     [rewrite > true_to_sigma_p_Sn
1170       [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
1171         [rewrite > sym_plus.
1172          rewrite > plus_minus
1173           [apply le_plus_to_minus_r.
1174            rewrite < plus_minus_m_m
1175             [rewrite > sym_plus.
1176              apply le_log_exp_Sn_log_exp_n.
1177
1178
1179 * a generalization
1180 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
1181 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
1182 intros.
1183 rewrite > exp_S_sigma_p.
1184 apply le_sigma_p.
1185 intros.unfold bc.
1186 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
1187   [rewrite > sym_times.
1188    apply le_times_r.
1189    rewrite > sym_times.
1190    rewrite < eq_div_div_div_times
1191     [apply monotonic_div
1192       [apply lt_O_fact
1193       |apply le_times_to_le_div2
1194         [apply lt_O_fact
1195         |apply le_fact_exp.
1196          apply le_S_S_to_le.
1197          assumption
1198         ]
1199       ]
1200     |apply lt_O_fact
1201     |apply lt_O_fact
1202     ]
1203   |apply le_times_div_div_times.
1204    apply lt_O_fact
1205   ]
1206 qed.
1207
1208 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
1209 (exp (S m) n) <
1210 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
1211 intros.
1212 rewrite > exp_S_sigma_p.
1213 apply lt_sigma_p
1214   [intros.unfold bc.
1215    apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
1216     [rewrite > sym_times.
1217      apply le_times_r.
1218      rewrite > sym_times.
1219      rewrite < eq_div_div_div_times
1220       [apply monotonic_div
1221         [apply lt_O_fact
1222         |apply le_times_to_le_div2
1223           [apply lt_O_fact
1224           |apply le_fact_exp.
1225            apply le_S_S_to_le.
1226            assumption
1227           ]
1228         ]
1229       |apply lt_O_fact
1230       |apply lt_O_fact
1231       ]
1232     |apply le_times_div_div_times.
1233      apply lt_O_fact
1234     ]
1235   |apply (ex_intro ? ? n).
1236    split
1237     [split
1238       [apply le_n
1239       |reflexivity
1240       ]
1241     |rewrite < minus_n_n.
1242      rewrite > bc_n_n.
1243      simplify.unfold lt.
1244      apply le_times_to_le_div
1245       [apply lt_O_fact
1246       |rewrite > sym_times.
1247        rewrite < plus_n_O.
1248        apply le_fact_exp1.
1249        assumption
1250       ]
1251     ]
1252   ]
1253 qed.
1254
1255 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
1256 (exp (S m) n) < (S(S(S O)))*(exp m n).
1257 intros.
1258 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
1259   [apply lt_exp_sigma_p_exp_m.assumption
1260   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
1261     [apply le_sigma_p.intros.
1262      apply le_times_to_le_div
1263       [apply lt_O_exp.
1264        apply lt_O_S
1265       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
1266         [apply le_times_div_div_times.
1267          apply lt_O_fact
1268         |apply le_times_to_le_div2
1269           [apply lt_O_fact
1270           |rewrite < sym_times.
1271            apply le_times_r.
1272            apply le_exp_SSO_fact
1273           ]
1274         ]
1275       ]
1276     |rewrite > eq_sigma_p_pred
1277       [rewrite > div_SO.
1278        rewrite > sym_plus.
1279        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
1280        apply le_plus_r.
1281        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)))
1282         [apply sigma_p_div_exp
1283         |apply le_times_to_le_div2
1284           [apply lt_O_exp.
1285            apply lt_O_S.
1286           |apply le_minus_m
1287           ]
1288         ]
1289       |reflexivity
1290       ]
1291     ]
1292   ]
1293 qed.
1294 *)