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