helm/software/matita/library/nat/chebyshev.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 (*       \ /        Matita 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/chebishev".
  16
  17 include "nat/log.ma".
  18 include "nat/pi_p.ma".
  19 include "nat/factorization.ma".
  20 include "nat/factorial2.ma".
  21
  22 definition prim: nat \to nat \def
  23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
  24
  25 definition A: nat \to nat \def
  26 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
  27
  28 theorem le_Al1: \forall n.
  29 A n \le pi_p (S n) primeb (\lambda p.n).
  30 intro.unfold A.
  31 cases n
  32   [simplify.apply le_n
  33   |apply le_pi_p.
  34    intros.
  35    apply le_exp_log.
  36    apply lt_O_S
  37   ]
  38 qed.
  39
  40 theorem le_Al: \forall n.
  41 A n \le exp n (prim n).
  42 intro.unfold prim.
  43 rewrite < exp_sigma_p.
  44 apply le_Al1.
  45 qed.
  46
  47 theorem leA_r2: \forall n.
  48 exp n (prim n) \le A n * A n.
  49 intro.unfold prim.
  50 elim (le_to_or_lt_eq ? ? (le_O_n n))
  51   [rewrite < (exp_sigma_p (S n) n primeb).
  52    unfold A.
  53    rewrite < times_pi_p.
  54    apply le_pi_p.
  55    intros.
  56    rewrite < exp_plus_times.
  57    apply (trans_le ? (exp i (S(log i n))))
  58     [apply lt_to_le.
  59      apply lt_exp_log.
  60      apply prime_to_lt_SO.
  61      apply primeb_true_to_prime.
  62      assumption
  63     |apply le_exp
  64       [apply prime_to_lt_O.
  65        apply primeb_true_to_prime.
  66        assumption
  67       |rewrite > plus_n_O.
  68        simplify.
  69        rewrite > plus_n_Sm.
  70        apply le_plus_r.
  71        apply lt_O_log
  72         [assumption
  73         |apply le_S_S_to_le.
  74          apply H1
  75         ]
  76       ]
  77     ]
  78   |rewrite < H. apply le_n
  79   ]
  80 qed.
  81
  82 definition A': nat \to nat \def
  83 \lambda n. pi_p (S n) primeb
  84   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
  85
  86 theorem eq_A_A': \forall n.A n = A' n.
  87 intro.unfold A.unfold A'.
  88 apply eq_pi_p
  89   [intros.reflexivity
  90   |intros.
  91    apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
  92     [apply eq_f.apply sym_eq.apply sigma_p_true
  93     |apply sym_eq.apply exp_sigma_p
  94     ]
  95   ]
  96 qed.
  97
  98 theorem eq_pi_p_primeb_divides_b: \forall n,m.
  99 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
 100 = pi_p n primeb (\lambda p.exp p (ord m p)).
 101 intro.
 102 elim n
 103   [reflexivity
 104   |apply (bool_elim ? (primeb n1));intro
 105     [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
 106       [apply (bool_elim ? (divides_b n1 m));intro
 107         [rewrite > true_to_pi_p_Sn
 108           [apply eq_f.
 109            apply H
 110           |apply true_to_true_to_andb_true;assumption
 111           ]
 112         |rewrite > false_to_pi_p_Sn
 113           [rewrite > not_divides_to_ord_O
 114             [simplify in ⊢ (? ? ? (? % ?)).
 115              rewrite > sym_times.
 116              rewrite < times_n_SO.
 117              apply H
 118             |apply primeb_true_to_prime.assumption
 119             |apply divides_b_false_to_not_divides.
 120              assumption
 121             ]
 122           |rewrite > H1.rewrite > H2.reflexivity
 123           ]
 124         ]
 125       |assumption
 126       ]
 127     |rewrite > false_to_pi_p_Sn
 128       [rewrite > false_to_pi_p_Sn
 129         [apply H
 130         |assumption
 131         ]
 132       |rewrite > H1.reflexivity
 133       ]
 134     ]
 135   ]
 136 qed.
 137
 138 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
 139 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
 140 intro.elim q
 141   [apply False_ind.
 142    apply (not_le_Sn_O ? H1)
 143   |apply (bool_elim ? (primeb n∧divides_b n m));intro
 144     [rewrite > true_to_pi_p_Sn
 145       [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
 146         [apply eq_f.
 147          rewrite > (H (ord_rem m n))
 148           [apply eq_pi_p1
 149             [intros.
 150              apply (bool_elim ? (primeb x));intro
 151               [simplify.
 152                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
 153                 [apply sym_eq.
 154                  apply divides_to_divides_b_true
 155                   [apply prime_to_lt_O.
 156                    apply primeb_true_to_prime.
 157                    assumption
 158                   |apply (trans_divides ? (ord_rem m n))
 159                     [apply divides_b_true_to_divides.
 160                      assumption
 161                     |apply divides_ord_rem
 162                       [apply (trans_lt ? x)
 163                         [apply prime_to_lt_SO.
 164                          apply primeb_true_to_prime.
 165                          assumption
 166                         |assumption
 167                         ]
 168                       |assumption
 169                       ]
 170                     ]
 171                   ]
 172                 |apply sym_eq.
 173                  apply not_divides_to_divides_b_false
 174                   [apply prime_to_lt_O.
 175                    apply primeb_true_to_prime.
 176                    assumption
 177                   |apply ord_O_to_not_divides
 178                     [assumption
 179                     |apply primeb_true_to_prime.
 180                      assumption
 181                     |rewrite < (ord_ord_rem n)
 182                       [apply not_divides_to_ord_O
 183                         [apply primeb_true_to_prime.
 184                          assumption
 185                         |apply divides_b_false_to_not_divides.
 186                          assumption
 187                         ]
 188                       |assumption
 189                       |apply primeb_true_to_prime.
 190                        apply (andb_true_true ? ? H3)
 191                       |apply primeb_true_to_prime.
 192                        assumption
 193                       |assumption
 194                       ]
 195                     ]
 196                   ]
 197                 ]
 198               |reflexivity
 199               ]
 200             |intros.
 201              apply eq_f.
 202              apply ord_ord_rem
 203               [assumption
 204               |apply primeb_true_to_prime.
 205                apply (andb_true_true ? ? H3)
 206               |apply primeb_true_to_prime.
 207                apply (andb_true_true ? ? H5)
 208               |assumption
 209               ]
 210             ]
 211           |apply lt_O_ord_rem
 212             [apply prime_to_lt_SO.
 213              apply primeb_true_to_prime.
 214              apply (andb_true_true ? ? H3)
 215             |assumption
 216             ]
 217           |apply not_eq_to_le_to_lt
 218             [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
 219               [elim H4.
 220                intro.rewrite > H7 in H6.simplify in H6.
 221                apply (not_divides_ord_rem m n)
 222                 [assumption
 223                 |apply prime_to_lt_SO.
 224                  apply primeb_true_to_prime.
 225                  apply (andb_true_true ? ? H3)
 226                 |apply divides_b_true_to_divides.
 227                  apply (andb_true_true_r ? ? H6)
 228                 ]
 229               |elim H4.rewrite > H6.
 230                apply lt_to_not_eq.
 231                apply prime_to_lt_O.
 232                apply primeb_true_to_prime.
 233                apply (andb_true_true ? ? H3)
 234               ]
 235             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
 236               [apply le_to_le_max.
 237                apply divides_to_le
 238                 [assumption
 239                 |apply divides_ord_rem
 240                   [apply prime_to_lt_SO.
 241                    apply primeb_true_to_prime.
 242                    apply (andb_true_true ? ? H3)
 243                   |assumption
 244                   ]
 245                 ]
 246               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
 247                 [apply le_max_f_max_g.
 248                  intros.
 249                  apply (bool_elim ? (primeb i));intro
 250                   [simplify.
 251                    apply divides_to_divides_b_true
 252                     [apply prime_to_lt_O.
 253                      apply primeb_true_to_prime.
 254                      assumption
 255                     |apply (trans_divides ? (ord_rem m n))
 256                       [apply divides_b_true_to_divides.
 257                        apply (andb_true_true_r ? ? H5)
 258                       |apply divides_ord_rem
 259                         [apply prime_to_lt_SO.
 260                          apply primeb_true_to_prime.
 261                          apply (andb_true_true ? ? H3)
 262                         |assumption
 263                         ]
 264                       ]
 265                     ]
 266                   |rewrite > H6 in H5.
 267                    assumption
 268                   ]
 269                 |apply le_S_S_to_le.
 270                  assumption
 271                 ]
 272               ]
 273             ]
 274           ]
 275         |apply prime_to_lt_SO.
 276          apply primeb_true_to_prime.
 277          apply (andb_true_true ? ? H3)
 278         |assumption
 279         ]
 280       |assumption
 281       ]
 282     |elim (le_to_or_lt_eq ? ? H1)
 283       [rewrite > false_to_pi_p_Sn
 284         [apply H
 285           [assumption
 286           |apply false_to_lt_max
 287             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
 288               [apply lt_to_le.
 289                apply lt_SO_max_prime.
 290                assumption
 291               |apply le_S_S_to_le.
 292                assumption
 293               ]
 294             |assumption
 295             |apply le_S_S_to_le.
 296              assumption
 297             ]
 298           ]
 299         |assumption
 300         ]
 301       |rewrite < H4.
 302        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
 303        apply eq_pi_p
 304         [intros.
 305          apply (bool_elim ? (primeb x));intro
 306           [apply sym_eq.
 307            change with (divides_b x (S O) =false).
 308            apply not_divides_to_divides_b_false
 309             [apply prime_to_lt_O.
 310              apply primeb_true_to_prime.
 311              assumption
 312             |intro.
 313              apply (le_to_not_lt x (S O))
 314               [apply divides_to_le
 315                 [apply lt_O_S.assumption
 316                 |assumption
 317                 ]
 318               |elim (primeb_true_to_prime ? H6).
 319                assumption
 320               ]
 321             ]
 322           |reflexivity
 323           ]
 324         |intros.reflexivity
 325         ]
 326       ]
 327     ]
 328   ]
 329 qed.
 330
 331 theorem pi_p_primeb_divides_b: \forall n. O < n \to
 332 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 333 intros.
 334 apply lt_max_to_pi_p_primeb
 335   [assumption
 336   |apply le_S_S.
 337    apply le_max_n
 338   ]
 339 qed.
 340
 341 theorem pi_p_primeb: \forall n. O < n \to
 342 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
 343 intros.
 344 rewrite < eq_pi_p_primeb_divides_b.
 345 apply pi_p_primeb_divides_b.
 346 assumption.
 347 qed.
 348
 349 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
 350 ord n p \le log p n.
 351 intros.
 352 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
 353   [rewrite > log_exp
 354     [apply le_plus_n_r
 355     |assumption
 356     |apply lt_O_ord_rem;assumption
 357     ]
 358   |assumption
 359   |assumption
 360   ]
 361 qed.
 362
 363 theorem sigma_p_divides_b:
 364 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
 365 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 366 intro.elim m
 367   [reflexivity
 368   |simplify in ⊢ (? ? ? (? % ? ?)).
 369    rewrite > true_to_sigma_p_Sn
 370     [rewrite > sym_plus.rewrite < plus_n_SO.
 371      apply eq_f.
 372      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
 373      apply eq_sigma_p1
 374       [intros.
 375        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
 376         [apply sym_eq.
 377          apply divides_to_divides_b_true
 378           [apply lt_O_exp.
 379            apply prime_to_lt_O.
 380            assumption
 381           |apply (witness ? ? ((exp p (n - x))*n1)).
 382            rewrite < assoc_times.
 383            rewrite < exp_plus_times.
 384            apply eq_f2
 385             [apply eq_f.simplify.
 386              apply eq_f.
 387              rewrite > sym_plus.
 388              apply plus_minus_m_m.
 389              apply lt_to_le.assumption
 390             |reflexivity
 391             ]
 392           ]
 393         |apply sym_eq.
 394          apply False_ind.
 395          apply (divides_b_false_to_not_divides ? ? H5).
 396          apply (witness ? ? ((exp p (n - S x))*n1)).
 397          rewrite < assoc_times.
 398          rewrite < exp_plus_times.
 399          apply eq_f2
 400           [apply eq_f.
 401            rewrite > sym_plus.
 402            apply plus_minus_m_m.
 403            assumption
 404           |reflexivity
 405           ]
 406         ]
 407       |intros.reflexivity
 408       ]
 409     |apply divides_to_divides_b_true
 410       [apply lt_O_exp.
 411        apply prime_to_lt_O.assumption
 412       |apply (witness ? ? n1).reflexivity
 413       ]
 414     ]
 415   ]
 416 qed.
 417
 418 theorem sigma_p_divides_b1:
 419 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
 420 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 421 intros.
 422 lapply (prime_to_lt_SO ? H1) as H4.
 423 lapply (prime_to_lt_O ? H1) as H5.
 424 rewrite > (false_to_eq_sigma_p m k)
 425   [apply sigma_p_divides_b;assumption
 426   |assumption
 427   |intros.
 428    apply not_divides_to_divides_b_false
 429     [apply lt_O_exp.assumption
 430     |intro.apply (le_to_not_lt ? ? H6).
 431      unfold lt.
 432      rewrite < (ord_exp p)
 433       [rewrite > (plus_n_O m).
 434        rewrite < (not_divides_to_ord_O ? ? H1 H2).
 435        rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
 436        rewrite < ord_times
 437         [apply divides_to_le_ord
 438           [apply lt_O_exp.assumption
 439           |rewrite > (times_n_O O).
 440            apply lt_times
 441             [apply lt_O_exp.assumption
 442             |assumption
 443             ]
 444           |assumption
 445           |assumption
 446           ]
 447         |apply lt_O_exp.assumption
 448         |assumption
 449         |assumption
 450         ]
 451       |assumption
 452       ]
 453     ]
 454   ]
 455 qed.
 456
 457 theorem eq_ord_sigma_p:
 458 \forall n,m,x. O < n \to prime x \to
 459 exp x m \le n \to n < exp x (S m) \to
 460 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
 461 intros.
 462 lapply (prime_to_lt_SO ? H1).
 463 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
 464   [apply sigma_p_divides_b1
 465     [apply lt_O_ord_rem;assumption
 466     |assumption
 467     |apply not_divides_ord_rem;assumption
 468     |apply lt_S_to_le.
 469      apply (le_to_lt_to_lt ? (log x n))
 470       [apply le_ord_log;assumption
 471       |apply (lt_exp_to_lt x)
 472         [assumption
 473         |apply (le_to_lt_to_lt ? n ? ? H3).
 474          apply le_exp_log.
 475          assumption
 476         ]
 477       ]
 478     ]
 479   |assumption
 480   |assumption
 481   ]
 482 qed.
 483
 484 theorem pi_p_primeb1: \forall n. O < n \to
 485 n = pi_p (S n) primeb
 486   (\lambda p.(pi_p (log p n)
 487     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
 488 intros.
 489 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
 490 apply eq_pi_p1
 491   [intros.reflexivity
 492   |intros.
 493    rewrite > exp_sigma_p.
 494    apply eq_f.
 495    apply eq_ord_sigma_p
 496     [assumption
 497     |apply primeb_true_to_prime.
 498      assumption
 499     |apply le_exp_log.assumption
 500     |apply lt_exp_log.
 501      apply prime_to_lt_SO.
 502      apply primeb_true_to_prime.
 503      assumption
 504     ]
 505   ]
 506 qed.
 507
 508 theorem eq_fact_pi_p:\forall n. fact n =
 509 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 510 intro.elim n
 511   [reflexivity
 512   |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
 513    rewrite > true_to_pi_p_Sn
 514     [apply eq_f.assumption
 515     |reflexivity
 516     ]
 517   ]
 518 qed.
 519
 520 theorem eq_sigma_p_div: \forall n,q.O < q \to
 521 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
 522 =n/q.
 523 intros.
 524 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 525   [apply div_mod_spec_intro
 526     [apply lt_mod_m_m.assumption
 527     |elim n
 528       [simplify.elim q;reflexivity
 529       |elim (or_div_mod1 n1 q)
 530         [elim H2.clear H2.
 531          rewrite > divides_to_mod_O
 532           [rewrite < plus_n_O.
 533            rewrite > true_to_sigma_p_Sn
 534             [rewrite > H4 in ⊢ (? ? % ?).
 535              apply eq_f2
 536               [rewrite < sym_plus.
 537                rewrite < plus_n_SO.
 538                apply eq_f.
 539                apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 540                 [apply div_mod_spec_div_mod.
 541                  assumption
 542                 |apply div_mod_spec_intro
 543                   [apply lt_mod_m_m.assumption
 544                   |assumption
 545                   ]
 546                 ]
 547               |reflexivity
 548               ]
 549             |apply true_to_true_to_andb_true
 550               [reflexivity
 551               |apply divides_to_divides_b_true;assumption
 552               ]
 553             ]
 554           |assumption
 555           |assumption
 556           ]
 557         |elim H2.clear H2.
 558          rewrite > false_to_sigma_p_Sn
 559           [rewrite > mod_S
 560             [rewrite < plus_n_Sm.
 561              apply eq_f.
 562              assumption
 563             |assumption
 564             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
 565               [assumption
 566               |apply False_ind.
 567                apply H3.
 568                apply (witness ? ? (S(div n1 q))).
 569                rewrite < times_n_Sm.
 570                rewrite < sym_plus.
 571                rewrite < H2 in ⊢ (? ? ? (? ? %)).
 572                rewrite > sym_times.
 573                assumption
 574               |apply lt_mod_m_m.
 575                assumption
 576               ]
 577             ]
 578           |rewrite > not_divides_to_divides_b_false
 579             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
 580             |assumption
 581             |assumption
 582             ]
 583           ]
 584         |assumption
 585         ]
 586       ]
 587     ]
 588   |apply div_mod_spec_div_mod.
 589    assumption
 590   ]
 591 qed.
 592
 593 theorem fact_pi_p: \forall n. fact n =
 594 pi_p (S n) primeb
 595   (\lambda p.(pi_p (log p n)
 596     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
 597 intros.
 598 rewrite > eq_fact_pi_p.
 599 apply (trans_eq ? ?
 600   (pi_p (S n) (λi:nat.leb (S O) i)
 601    (λn.pi_p (S n) primeb
 602     (\lambda p.(pi_p (log p n)
 603      (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
 604   [apply eq_pi_p1;intros
 605     [reflexivity
 606     |apply pi_p_primeb1.
 607      apply leb_true_to_le.assumption
 608     ]
 609   |apply (trans_eq ? ?
 610     (pi_p (S n) (λi:nat.leb (S O) i)
 611      (λn:nat
 612       .pi_p (S n) (\lambda p.primeb p\land leb p n)
 613        (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
 614     [apply eq_pi_p1
 615       [intros.reflexivity
 616       |intros.apply eq_pi_p1
 617         [intros.elim (primeb x1)
 618           [simplify.apply sym_eq.
 619            apply le_to_leb_true.
 620            apply le_S_S_to_le.
 621            assumption
 622           |reflexivity
 623           ]
 624         |intros.reflexivity
 625         ]
 626       ]
 627     |apply (trans_eq ? ?
 628       (pi_p (S n) (λi:nat.leb (S O) i)
 629        (λm:nat
 630         .pi_p (S n) (λp:nat.primeb p∧leb p m)
 631          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
 632       [apply eq_pi_p1
 633         [intros.reflexivity
 634         |intros.
 635          apply sym_eq.
 636          apply false_to_eq_pi_p
 637           [assumption
 638           |intros.rewrite > lt_to_leb_false
 639             [elim primeb;reflexivity|assumption]
 640           ]
 641         ]
 642       |(* make a general theorem *)
 643        apply (trans_eq ? ?
 644         (pi_p (S n) primeb
 645          (λp:nat
 646           .pi_p (S n) (λm.leb p m)
 647            (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
 648         ))
 649         [apply pi_p_pi_p1.
 650          intros.
 651          apply (bool_elim ? (primeb y \land leb y x));intros
 652           [rewrite > (le_to_leb_true (S O) x)
 653             [reflexivity
 654             |apply (trans_le ? y)
 655               [apply prime_to_lt_O.
 656                apply primeb_true_to_prime.
 657                apply (andb_true_true ? ? H2)
 658               |apply leb_true_to_le.
 659                apply (andb_true_true_r ? ? H2)
 660               ]
 661             ]
 662           |elim (leb (S O) x);reflexivity
 663           ]
 664         |apply eq_pi_p1
 665           [intros.reflexivity
 666           |intros.
 667            apply (trans_eq ? ?
 668             (pi_p (S n) (λm:nat.leb x m)
 669              (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
 670             [apply eq_pi_p1
 671               [intros.reflexivity
 672               |intros.
 673                apply sym_eq.
 674                apply false_to_eq_pi_p
 675                 [apply le_log
 676                   [apply prime_to_lt_SO.
 677                    apply primeb_true_to_prime.
 678                    assumption
 679                   |apply (lt_to_le_to_lt ? x)
 680                     [apply prime_to_lt_O.
 681                      apply primeb_true_to_prime.
 682                      assumption
 683                     |apply leb_true_to_le.
 684                      assumption
 685                     ]
 686                   |apply le_S_S_to_le.
 687                    assumption
 688                   ]
 689                 |intros.
 690                  apply not_divides_to_divides_b_false
 691                   [apply lt_O_exp.
 692                    apply prime_to_lt_O.
 693                    apply primeb_true_to_prime.
 694                    assumption
 695                   |intro.
 696                    apply (lt_to_not_le x1 (exp x (S i)))
 697                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
 698                       [apply lt_exp_log.
 699                        apply prime_to_lt_SO.
 700                        apply primeb_true_to_prime.
 701                        assumption
 702                       |apply le_exp
 703                         [apply prime_to_lt_O.
 704                          apply primeb_true_to_prime.
 705                          assumption
 706                         |apply le_S_S.
 707                          assumption
 708                         ]
 709                       ]
 710                     |apply divides_to_le
 711                       [apply (lt_to_le_to_lt ? x)
 712                         [apply prime_to_lt_O.
 713                          apply primeb_true_to_prime.
 714                          assumption
 715                         |apply leb_true_to_le.
 716                          assumption
 717                         ]
 718                       |assumption
 719                       ]
 720                     ]
 721                   ]
 722                 ]
 723               ]
 724             |apply
 725              (trans_eq ? ?
 726               (pi_p (log x n) (λi:nat.true)
 727                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
 728               [apply (pi_p_pi_p1 (\lambda m,i.x)).
 729                intros.
 730                reflexivity
 731               |apply eq_pi_p1
 732                 [intros.reflexivity
 733                 |intros.
 734                  rewrite > exp_sigma_p.
 735                  apply eq_f.
 736                  apply (trans_eq ? ?
 737                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
 738                   [apply eq_sigma_p1
 739                     [intros.
 740                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
 741                       [apply (bool_elim ? (leb x x2));intro
 742                         [rewrite > le_to_leb_true
 743                           [reflexivity
 744                           |apply (trans_le ? x)
 745                             [apply prime_to_lt_O.
 746                              apply primeb_true_to_prime.
 747                              assumption
 748                             |apply leb_true_to_le.
 749                              assumption
 750                             ]
 751                           ]
 752                         |rewrite > lt_to_leb_false
 753                           [reflexivity
 754                           |apply not_le_to_lt.intro.
 755                            apply (leb_false_to_not_le ? ? H6).
 756                            apply (trans_le ? (exp x (S x1)))
 757                             [rewrite > times_n_SO in ⊢ (? % ?).
 758                              change with (exp x (S O) \le exp x (S x1)).
 759                              apply le_exp
 760                               [apply prime_to_lt_O.
 761                                apply primeb_true_to_prime.
 762                                assumption
 763                               |apply le_S_S.apply le_O_n.
 764                               ]
 765                             |apply divides_to_le
 766                               [assumption
 767                               |apply divides_b_true_to_divides.
 768                                assumption
 769                               ]
 770                             ]
 771                           ]
 772                         ]
 773                       |rewrite < andb_sym.
 774                        rewrite < andb_sym in ⊢ (? ? ? %).
 775                        reflexivity
 776                       ]
 777                     |intros.reflexivity
 778                     ]
 779                   |apply eq_sigma_p_div.
 780                    apply lt_O_exp.
 781                    apply prime_to_lt_O.
 782                    apply primeb_true_to_prime.
 783                    assumption
 784                   ]
 785                 ]
 786               ]
 787             ]
 788           ]
 789         ]
 790       ]
 791     ]
 792   ]
 793 qed.
 794
 795 (* odd n is just mod n (S(S O))
 796 let rec odd n \def
 797   match n with
 798   [ O \Rightarrow O
 799   | S m \Rightarrow (S O) - odd m
 800   ].
 801
 802 theorem le_odd_SO: \forall n. odd n \le S O.
 803 intro.elim n
 804   [apply le_O_n
 805   |simplify.cases (odd n1)
 806     [simplify.apply le_n.
 807     |apply le_O_n
 808     ]
 809   ]
 810 qed.
 811
 812 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
 813 intro.elim n
 814   [apply (lt_O_n_elim ? H).
 815    intro.simplify.reflexivity
 816   |
 817 *)
 818
 819 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
 820 pi_p (S ((S(S O))*n)) primeb
 821   (\lambda p.(pi_p (log p ((S(S O))*n))
 822     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
 823 intros.rewrite > fact_pi_p.
 824 apply eq_pi_p1
 825   [intros.reflexivity
 826   |intros.apply eq_pi_p
 827     [intros.reflexivity
 828     |intros.
 829      rewrite < exp_plus_times.
 830      apply eq_f.
 831      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 832      apply SSO_mod.
 833      apply lt_O_exp.
 834      apply prime_to_lt_O.
 835      apply primeb_true_to_prime.
 836      assumption
 837     ]
 838   ]
 839 qed.
 840
 841 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
 842 pi_p (S ((S(S O))*n)) primeb
 843   (\lambda p.(pi_p (log p ((S(S O))*n))
 844     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
 845 pi_p (S ((S(S O))*n)) primeb
 846   (\lambda p.(pi_p (log p ((S(S O))*n))
 847     (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
 848 intros.
 849 rewrite < times_pi_p.
 850 rewrite > fact_pi_p2.
 851 apply eq_pi_p;intros
 852   [reflexivity
 853   |apply times_pi_p
 854   ]
 855 qed.
 856
 857 theorem pi_p_primeb4: \forall n. S O < n \to
 858 pi_p (S ((S(S O))*n)) primeb
 859   (\lambda p.(pi_p (log p ((S(S O))*n))
 860     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 861 =
 862 pi_p (S n) primeb
 863   (\lambda p.(pi_p (log p (S(S O)*n))
 864     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 865 intros.
 866 apply or_false_eq_SO_to_eq_pi_p
 867   [apply le_S_S.
 868    apply le_times_n.
 869    apply lt_O_S
 870   |intros.
 871    right.
 872    rewrite > log_i_SSOn
 873     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
 874      rewrite < times_n_SO.
 875      rewrite > eq_div_O
 876       [reflexivity
 877       |simplify.rewrite < times_n_SO.assumption
 878       ]
 879     |assumption
 880     |assumption
 881     |apply le_S_S_to_le.assumption
 882     ]
 883   ]
 884 qed.
 885
 886 theorem pi_p_primeb5: \forall n. S O < n \to
 887 pi_p (S ((S(S O))*n)) primeb
 888   (\lambda p.(pi_p (log p ((S(S O))*n))
 889     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 890 =
 891 pi_p (S n) primeb
 892   (\lambda p.(pi_p (log p n)
 893     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 894 intros.
 895 rewrite > (pi_p_primeb4 ? H).
 896 apply eq_pi_p1;intros
 897   [reflexivity
 898   |apply or_false_eq_SO_to_eq_pi_p
 899     [apply le_log
 900       [apply prime_to_lt_SO.
 901        apply primeb_true_to_prime.
 902        assumption
 903       |apply lt_to_le.assumption
 904       |apply le_times_n.
 905        apply lt_O_S
 906       ]
 907     |intros.right.
 908      rewrite > eq_div_O
 909       [simplify.reflexivity
 910       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
 911         [apply lt_exp_log.
 912          apply prime_to_lt_SO.
 913          apply primeb_true_to_prime.
 914          assumption
 915         |apply le_exp
 916           [apply prime_to_lt_O.
 917            apply primeb_true_to_prime.
 918            assumption
 919           |apply le_S_S.
 920            assumption
 921           ]
 922         ]
 923       ]
 924     ]
 925   ]
 926 qed.
 927
 928 theorem exp_fact_SSO: \forall n.
 929 exp (fact n) (S(S O))
 930 =
 931 pi_p (S n) primeb
 932   (\lambda p.(pi_p (log p n)
 933     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 934 intros.
 935 rewrite > fact_pi_p.
 936 rewrite < exp_pi_p.
 937 apply eq_pi_p;intros
 938   [reflexivity
 939   |apply sym_eq.
 940    apply exp_times_pi_p
 941   ]
 942 qed.
 943
 944 definition B \def
 945 \lambda n.
 946 pi_p (S n) primeb
 947   (\lambda p.(pi_p (log p n)
 948     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 949
 950 theorem eq_fact_B:\forall n.S O < n \to
 951 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 952 intros. unfold B.
 953 rewrite > fact_pi_p3.
 954 apply eq_f2
 955   [apply sym_eq.
 956    rewrite > pi_p_primeb5
 957     [apply exp_fact_SSO
 958     |assumption
 959     ]
 960   |reflexivity
 961   ]
 962 qed.
 963
 964 theorem le_B_A: \forall n. B n \le A n.
 965 intro.unfold B.
 966 rewrite > eq_A_A'.
 967 unfold A'.
 968 apply le_pi_p.intros.
 969 apply le_pi_p.intros.
 970 rewrite > exp_n_SO in ⊢ (? ? %).
 971 apply le_exp
 972   [apply prime_to_lt_O.
 973    apply primeb_true_to_prime.
 974    assumption
 975   |apply le_S_S_to_le.
 976    apply lt_mod_m_m.
 977    apply lt_O_S
 978   ]
 979 qed.
 980
 981 theorem le_fact_A:\forall n.S O < n \to
 982 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
 983 intros.
 984 rewrite > eq_fact_B
 985   [apply le_times_r.
 986    apply le_B_A
 987   |assumption
 988   ]
 989 qed.
 990
 991 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 992 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
 993 intros.
 994 apply (le_times_to_le (exp (fact n) (S(S O))))
 995   [apply lt_O_exp.
 996    apply lt_O_fact
 997   |rewrite < eq_fact_B
 998     [rewrite < sym_times in ⊢ (? ? %).
 999      rewrite > exp_SSO.
1000      rewrite < assoc_times.
1001      apply fact1
1002     |assumption
1003     ]
1004   ]
1005 qed.
1006
1007 theorem le_B_exp: \forall n.
1008 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1009 intro.cases n
1010   [apply le_n
1011   |cases n1
1012     [simplify.apply le_S.apply le_S.apply le_n
1013     |apply lt_SO_to_le_B_exp.
1014      apply le_S_S.apply lt_O_S.
1015     ]
1016   ]
1017 qed.
1018
1019 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1020 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1021 intros.
1022 apply (le_times_to_le (exp (fact n) (S(S O))))
1023   [apply lt_O_exp.
1024    apply lt_O_fact
1025   |rewrite < assoc_times in ⊢ (? ? %).
1026    rewrite > sym_times in ⊢ (? ? (? % ?)).
1027    rewrite > assoc_times in ⊢ (? ? %).
1028    rewrite < eq_fact_B
1029     [rewrite < sym_times.
1030      apply fact3.
1031      apply lt_to_le.assumption
1032     |assumption
1033     ]
1034   ]
1035 qed.
1036
1037 theorem le_exp_B: \forall n. O < n \to
1038 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1039 intros.
1040 elim H
1041   [apply le_n
1042   |apply lt_SO_to_le_exp_B.
1043    apply le_S_S.assumption
1044   ]
1045 qed.
1046
1047 theorem eq_A_SSO_n: \forall n.O < n \to
1048 A((S(S O))*n) =
1049  pi_p (S ((S(S O))*n)) primeb
1050   (\lambda p.(pi_p (log p ((S(S O))*n) )
1051     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1052  *A n.
1053 intro.
1054 rewrite > eq_A_A'.rewrite > eq_A_A'.
1055 unfold A'.intros.
1056 cut (
1057  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1058  = pi_p (S ((S(S O))*n)) primeb
1059     (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
1060   [rewrite > Hcut.
1061    rewrite < times_pi_p.
1062    apply eq_pi_p1;intros
1063     [reflexivity
1064     |rewrite < times_pi_p.
1065      apply eq_pi_p;intros
1066       [reflexivity
1067       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1068         [simplify.rewrite < times_n_SO.apply times_n_SO
1069         |simplify.rewrite < plus_n_O.apply times_n_SO
1070         ]
1071       ]
1072     ]
1073   |apply (trans_eq ? ? (pi_p (S n) primeb
1074     (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
1075     [apply eq_pi_p1;intros
1076       [reflexivity
1077       |apply eq_pi_p1;intros
1078         [reflexivity
1079         |rewrite > lt_to_leb_false
1080           [simplify.apply times_n_SO
1081           |apply le_S_S.
1082            apply (trans_le ? (exp x (log x n)))
1083             [apply le_exp
1084               [apply prime_to_lt_O.
1085                apply primeb_true_to_prime.
1086                assumption
1087               |assumption
1088               ]
1089             |apply le_exp_log.
1090              assumption
1091             ]
1092           ]
1093         ]
1094       ]
1095     |apply (trans_eq ? ?
1096       (pi_p (S ((S(S O))*n)) primeb
1097        (λp:nat.pi_p (log p n) (λi:nat.true)
1098         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1099       [apply sym_eq.
1100        apply or_false_eq_SO_to_eq_pi_p
1101         [apply le_S_S.
1102          simplify.
1103          apply le_plus_n_r
1104         |intros.right.
1105          rewrite > lt_to_log_O
1106           [reflexivity
1107           |assumption
1108           |assumption
1109           ]
1110         ]
1111       |apply eq_pi_p1;intros
1112         [reflexivity
1113         |apply sym_eq.
1114          apply or_false_eq_SO_to_eq_pi_p
1115           [apply le_log
1116             [apply prime_to_lt_SO.
1117              apply primeb_true_to_prime.
1118              assumption
1119             |assumption
1120             |simplify.
1121              apply le_plus_n_r
1122             ]
1123           |intros.right.
1124            rewrite > le_to_leb_true
1125             [simplify.reflexivity
1126             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1127               [apply lt_exp_log.
1128                apply prime_to_lt_SO.
1129                apply primeb_true_to_prime.
1130                assumption
1131               |apply le_exp
1132                 [apply prime_to_lt_O.
1133                  apply primeb_true_to_prime.
1134                  assumption
1135                 |apply le_S_S.assumption
1136                 ]
1137               ]
1138             ]
1139           ]
1140         ]
1141       ]
1142     ]
1143   ]
1144 qed.
1145
1146 theorem le_A_BA1: \forall n. O < n \to
1147 A((S(S O))*n) \le B((S(S O))*n)*A n.
1148 intros.
1149 rewrite > eq_A_SSO_n
1150   [apply le_times_l.
1151    unfold B.
1152    apply le_pi_p.intros.
1153    apply le_pi_p.intros.
1154    apply le_exp
1155     [apply prime_to_lt_O.
1156      apply primeb_true_to_prime.
1157      assumption
1158     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1159       [simplify in ⊢ (? % ?).
1160        cut ((S(S O))*n/i\sup(S i1) = S O)
1161         [rewrite > Hcut.apply le_n
1162         |apply (div_mod_spec_to_eq
1163           ((S(S O))*n) (exp i (S i1))
1164            ? (mod ((S(S O))*n) (exp i (S i1)))
1165            ? (minus ((S(S O))*n) (exp i (S i1))) )
1166           [apply div_mod_spec_div_mod.
1167            apply lt_O_exp.
1168            apply prime_to_lt_O.
1169            apply primeb_true_to_prime.
1170            assumption
1171           |cut (i\sup(S i1)≤(S(S O))*n)
1172             [apply div_mod_spec_intro
1173               [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
1174                apply lt_plus_to_lt_minus
1175                 [assumption
1176                 |simplify in ⊢ (? % ?).
1177                  rewrite < plus_n_O.
1178                  apply lt_plus
1179                   [apply leb_true_to_le.assumption
1180                   |apply leb_true_to_le.assumption
1181                   ]
1182                 ]
1183               |rewrite > sym_plus.
1184                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1185                rewrite < times_n_SO.
1186                apply plus_minus_m_m.
1187                assumption
1188               ]
1189             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1190               [apply le_exp
1191                 [apply prime_to_lt_O.
1192                  apply primeb_true_to_prime.
1193                  assumption
1194                 |assumption
1195                 ]
1196               |apply le_exp_log.
1197                rewrite > (times_n_O O) in ⊢ (? % ?).
1198                apply lt_times
1199                 [apply lt_O_S
1200                 |assumption
1201                 ]
1202               ]
1203             ]
1204           ]
1205         ]
1206       |apply le_O_n
1207       ]
1208     ]
1209   |assumption
1210   ]
1211 qed.
1212
1213 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1214 intros.cases n
1215   [apply le_n
1216   |apply le_A_BA1.apply lt_O_S
1217   ]
1218 qed.
1219
1220 theorem le_A_exp: \forall n.
1221 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1222 intro.
1223 apply (trans_le ? (B((S(S O))*n)*A n))
1224   [apply le_A_BA
1225   |apply le_times_l.
1226    apply le_B_exp
1227   ]
1228 qed.
1229
1230 theorem le_A_exp1: \forall n.
1231 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1232 intro.elim n
1233   [simplify.apply le_S_S.apply le_O_n
1234   |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1235    apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1236     [apply le_A_exp
1237     |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
1238       [apply le_times_r.
1239        assumption
1240       |rewrite < exp_plus_times.
1241        simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1242        apply le_n
1243       ]
1244     ]
1245   ]
1246 qed.
1247
1248 theorem monotonic_A: monotonic nat le A.
1249 unfold.intros.
1250 elim H
1251   [apply le_n
1252   |apply (trans_le ? (A n1))
1253     [assumption
1254     |unfold A.
1255      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1256           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1257       [apply (bool_elim ? (primeb (S n1)));intro
1258         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1259          rewrite > times_n_SO in ⊢ (? % ?).
1260          rewrite > sym_times.
1261          apply le_times
1262           [apply lt_O_exp.apply lt_O_S
1263           |assumption
1264           ]
1265         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1266          assumption
1267         ]
1268       |apply le_pi_p.intros.
1269        apply le_exp
1270         [apply prime_to_lt_O.
1271          apply primeb_true_to_prime.
1272          assumption
1273         |apply le_log
1274           [apply prime_to_lt_SO.
1275            apply primeb_true_to_prime.
1276            assumption
1277           |apply (lt_to_le_to_lt ? i)
1278             [apply prime_to_lt_O.
1279              apply primeb_true_to_prime.
1280              assumption
1281             |apply le_S_S_to_le.
1282              assumption
1283             ]
1284           |apply le_S.apply le_n
1285           ]
1286         ]
1287       ]
1288     ]
1289   ]
1290 qed.
1291
1292 theorem le_A_exp2: \forall n. O < n \to
1293 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1294 intros.
1295 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1296   [apply monotonic_A.
1297    apply lt_to_le.
1298    apply lt_exp_log.
1299    apply le_n
1300   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1301     [apply le_A_exp1
1302     |apply le_exp
1303       [apply lt_O_S
1304       |rewrite > assoc_times.apply le_times_r.
1305        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1306        apply le_times_r.
1307        apply le_exp_log.
1308        assumption
1309       ]
1310     ]
1311   ]
1312 qed.
1313
1314 (* example *)
1315 theorem A_SO: A (S O) = S O.
1316 reflexivity.
1317 qed.
1318
1319 theorem A_SSO: A (S(S O)) = S (S O).
1320 reflexivity.
1321 qed.
1322
1323 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1324 reflexivity.
1325 qed.
1326
1327 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1328 reflexivity.
1329 qed.
1330
1331 (* da spostare *)
1332 theorem or_eq_eq_S: \forall n.\exists m.
1333 n = (S(S O))*m \lor n = S ((S(S O))*m).
1334 intro.elim n
1335   [apply (ex_intro ? ? O).
1336    left.reflexivity
1337   |elim H.elim H1
1338     [apply (ex_intro ? ? a).
1339      right.apply eq_f.assumption
1340     |apply (ex_intro ? ? (S a)).
1341      left.rewrite > H2.
1342      apply sym_eq.
1343      apply times_SSO
1344     ]
1345   ]
1346 qed.
1347
1348 (* a better result *)
1349 theorem le_A_exp3: \forall n. S O < n \to
1350 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1351 intro.
1352 apply (nat_elim1 n).
1353 intros.
1354 elim (or_eq_eq_S m).
1355 elim H2
1356   [elim (le_to_or_lt_eq (S O) a)
1357     [rewrite > H3 in ⊢ (? % ?).
1358      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1359       [apply le_A_exp
1360       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1361          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1362         [apply le_times_r.
1363          apply H
1364           [rewrite > H3.
1365            rewrite > times_n_SO in ⊢ (? % ?).
1366            rewrite > sym_times.
1367            apply lt_times_l1
1368             [apply lt_to_le.assumption
1369             |apply le_n
1370             ]
1371           |assumption
1372           ]
1373         |rewrite > sym_times.
1374          rewrite > assoc_times.
1375          rewrite < exp_plus_times.
1376          apply (trans_le ?
1377           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1378           [rewrite > assoc_times.
1379            apply le_times_r.
1380            rewrite < exp_plus_times.
1381            apply le_exp
1382             [apply lt_O_S
1383             |rewrite < H3.
1384              simplify.
1385              rewrite < plus_n_O.
1386              apply le_S.apply le_S.
1387              apply le_n
1388             ]
1389           |apply le_times_l.
1390            rewrite > times_exp.
1391            apply monotonic_exp1.
1392            rewrite > H3.
1393            rewrite > sym_times.
1394            cases a
1395             [apply le_n
1396             |simplify.
1397              rewrite < plus_n_Sm.
1398              apply le_S.
1399              apply le_n
1400             ]
1401           ]
1402         ]
1403       ]
1404     |rewrite < H4 in H3.
1405      simplify in H3.
1406      rewrite > H3.
1407      simplify.
1408      apply le_S_S.apply le_S_S.apply le_O_n
1409     |apply not_lt_to_le.intro.
1410      apply (lt_to_not_le ? ? H1).
1411      rewrite > H3.
1412      apply (le_n_O_elim a)
1413       [apply le_S_S_to_le.assumption
1414       |apply le_O_n
1415       ]
1416     ]
1417   |elim (le_to_or_lt_eq O a (le_O_n ?))
1418     [apply (trans_le ? (A ((S(S O))*(S a))))
1419       [apply monotonic_A.
1420        rewrite > H3.
1421        rewrite > times_SSO.
1422        apply le_n_Sn
1423       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1424         [apply le_A_exp
1425         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1426            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1427           [apply le_times_r.
1428            apply H
1429             [rewrite > H3.
1430              apply le_S_S.
1431              simplify.
1432              rewrite > plus_n_SO.
1433              apply le_plus_r.
1434              rewrite < plus_n_O.
1435              assumption
1436             |apply le_S_S.assumption
1437             ]
1438           |rewrite > sym_times.
1439            rewrite > assoc_times.
1440            rewrite < exp_plus_times.
1441            apply (trans_le ?
1442             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1443             [rewrite > assoc_times.
1444              apply le_times_r.
1445              rewrite < exp_plus_times.
1446              apply le_exp
1447               [apply lt_O_S
1448               |rewrite > times_SSO.
1449                rewrite < H3.
1450                simplify.
1451                rewrite < plus_n_Sm.
1452                rewrite < plus_n_O.
1453                apply le_n
1454               ]
1455             |apply le_times_l.
1456              rewrite > times_exp.
1457              apply monotonic_exp1.
1458              rewrite > H3.
1459              rewrite > sym_times.
1460              apply le_n
1461             ]
1462           ]
1463         ]
1464       ]
1465     |rewrite < H4 in H3.simplify in H3.
1466      apply False_ind.
1467      apply (lt_to_not_le ? ? H1).
1468      rewrite > H3.
1469      apply le_n
1470     ]
1471   ]
1472 qed.
1473
1474 theorem eq_sigma_pi_SO_n: \forall n.
1475 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1476 intro.elim n
1477   [reflexivity
1478   |rewrite > true_to_sigma_p_Sn
1479     [rewrite > H.reflexivity
1480     |reflexivity
1481     ]
1482   ]
1483 qed.
1484
1485 theorem leA_prim: \forall n.
1486 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1487 intro.
1488 unfold prim.
1489 rewrite < (exp_sigma_p (S n) n primeb).
1490 unfold A.
1491 rewrite < times_pi_p.
1492 apply le_pi_p.
1493 intros.
1494 rewrite > sym_times.
1495 change in ⊢ (? ? %) with (exp i (S (log i n))).
1496 apply lt_to_le.
1497 apply lt_exp_log.
1498 apply prime_to_lt_SO.
1499 apply primeb_true_to_prime.
1500 assumption.
1501 qed.
1502
1503
1504 (* the inequalities *)
1505 theorem le_exp_priml: \forall n. O < n \to
1506 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1507 intros.
1508 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1509   [apply le_exp_B.assumption
1510   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1511    apply le_times_r.
1512    apply (trans_le ? (A ((S(S O))*n)))
1513     [apply le_B_A
1514     |apply le_Al
1515     ]
1516   ]
1517 qed.
1518
1519 theorem le_priml: \forall n. O < n \to
1520 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1521 intros.
1522 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1523   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1524     [apply le_log
1525       [apply le_n
1526       |apply lt_O_exp.apply lt_O_S
1527       |apply le_exp_priml.assumption
1528       ]
1529     |rewrite > sym_times in ⊢ (? ? %).
1530      apply log_exp1.
1531      apply le_n
1532     ]
1533   |apply le_n
1534   ]
1535 qed.
1536
1537 theorem le_exp_primr: \forall n. S O < n \to
1538 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
1539 intros.
1540 apply (trans_le ? (exp (A n) (S(S O))))
1541   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1542    rewrite < times_n_SO.
1543    apply leA_r2
1544   |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
1545     [apply monotonic_exp1.
1546      apply le_A_exp3.
1547      assumption
1548     |rewrite < times_exp.
1549      rewrite > exp_exp_times.
1550      rewrite > exp_exp_times.
1551      rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1552      rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
1553      apply le_n
1554     ]
1555   ]
1556 qed.
1557
1558
1559 (* da spostare *)
1560 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
1561 intros.elim p
1562   [reflexivity
1563   |simplify.autobatch
1564   ]
1565 qed.
1566
1567 theorem le_exp_log: \forall p,n. O < n \to
1568 exp p (
1569 log n) \le n.
1570 intros.
1571 apply leb_true_to_le.
1572 unfold log.
1573 apply (f_max_true (\lambda x.leb (exp p x) n)).
1574 apply (ex_intro ? ? O).
1575 split
1576   [apply le_O_n
1577   |apply le_to_leb_true.simplify.assumption
1578   ]
1579 qed.
1580
1581 theorem lt_log_n_n: \forall n. O < n \to log n < n.
1582 intros.
1583 cut (log n \le n)
1584   [elim (le_to_or_lt_eq ? ? Hcut)
1585     [assumption
1586     |absurd (exp (S(S O)) n \le n)
1587       [rewrite < H1 in ⊢ (? (? ? %) ?).
1588        apply le_exp_log.
1589        assumption
1590       |apply lt_to_not_le.
1591        apply lt_m_exp_nm.
1592        apply le_n
1593       ]
1594     ]
1595   |unfold log.apply le_max_n
1596   ]
1597 qed.
1598
1599 theorem le_log_n_n: \forall n. log n \le n.
1600 intro.
1601 cases n
1602   [apply le_n
1603   |apply lt_to_le.
1604    apply lt_log_n_n.
1605    apply lt_O_S
1606   ]
1607 qed.
1608
1609 theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
1610 intro.cases n
1611   [simplify.apply le_S.apply le_n
1612   |apply not_le_to_lt.
1613    apply leb_false_to_not_le.
1614    apply (lt_max_to_false ? (S n1) (S (log (S n1))))
1615     [apply le_S_S.apply le_n
1616     |apply lt_log_n_n.apply lt_O_S
1617     ]
1618   ]
1619 qed.
1620
1621 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
1622 (\forall m. p < m \to f m = false)
1623 \to max n f \le p.
1624 intros.
1625 apply not_lt_to_le.intro.
1626 apply not_eq_true_false.
1627 rewrite < (H1 ? H2).
1628 apply sym_eq.
1629 apply f_max_true.
1630 assumption.
1631 qed.
1632
1633 theorem log_times1: \forall n,m. O < n \to O < m \to
1634 log (n*m) \le S(log n+log m).
1635 intros.
1636 unfold in ⊢ (? (% ?) ?).
1637 apply f_false_to_le_max
1638   [apply (ex_intro ? ? O).
1639    split
1640     [apply le_O_n
1641     |apply le_to_leb_true.
1642      simplify.
1643      rewrite > times_n_SO.
1644      apply le_times;assumption
1645     ]
1646   |intros.
1647    apply lt_to_leb_false.
1648    apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
1649     [apply lt_times;apply lt_exp_log
1650     |rewrite < exp_plus_times.
1651      apply le_exp
1652       [apply lt_O_S
1653       |simplify.
1654        rewrite < plus_n_Sm.
1655        assumption
1656       ]
1657     ]
1658   ]
1659 qed.
1660
1661 theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
1662 intros.
1663 cases n
1664   [apply le_O_n
1665   |cases m
1666     [rewrite < times_n_O.
1667      apply le_O_n
1668     |apply log_times1;apply lt_O_S
1669     ]
1670   ]
1671 qed.
1672
1673 theorem log_exp: \forall n,m.O < m \to
1674 log ((exp (S(S O)) n)*m)=n+log m.
1675 intros.
1676 unfold log in ⊢ (? ? (% ?) ?).
1677 apply max_spec_to_max.
1678 unfold max_spec.
1679 split
1680   [split
1681     [elim n
1682       [simplify.
1683        rewrite < plus_n_O.
1684        apply le_log_n_n
1685       |simplify.
1686        rewrite < plus_n_O.
1687        rewrite > times_plus_l.
1688        apply (trans_le ? (S((S(S O))\sup(n1)*m)))
1689         [apply le_S_S.assumption
1690         |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
1691           [rewrite > (times_n_O O) in ⊢ (? % ?).
1692            apply lt_times
1693             [apply lt_O_exp.
1694              apply lt_O_S
1695             |assumption
1696             ]
1697           |intro.simplify.apply le_S_S.
1698            apply le_plus_n
1699           ]
1700         ]
1701       ]
1702     |simplify.
1703      apply le_to_leb_true.
1704      rewrite > exp_plus_times.
1705      apply le_times_r.
1706      apply le_exp_log.
1707      assumption
1708     ]
1709   |intros.
1710    simplify.
1711    apply lt_to_leb_false.
1712    apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
1713     [apply lt_times_r1
1714       [apply lt_O_exp.apply lt_O_S
1715       |apply lt_exp_log.
1716       ]
1717     |rewrite < exp_plus_times.
1718      apply le_exp
1719       [apply lt_O_S
1720       |rewrite < plus_n_Sm.
1721        assumption
1722       ]
1723     ]
1724   ]
1725 qed.
1726
1727 theorem log_SSO: \forall n. O < n \to
1728 log ((S(S O))*n) = S (log n).
1729 intros.
1730 change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
1731 rewrite > log_exp.reflexivity.assumption.
1732 qed.
1733
1734 theorem or_eq_S: \forall n.\exists m.
1735 (n = (S(S O))*m) \lor (n = S((S(S O))*m)).
1736 intro.
1737 elim n
1738   [apply (ex_intro ? ? O).left.apply times_n_O
1739   |elim H.elim H1
1740     [apply (ex_intro ? ? a).right.apply eq_f.assumption
1741     |apply (ex_intro ? ? (S a)).left.
1742      rewrite > H2.simplify.
1743      rewrite < plus_n_O.
1744      rewrite < plus_n_Sm.
1745      reflexivity
1746     ]
1747   ]
1748 qed.
1749
1750 theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
1751 ((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
1752 intros.
1753 elim (or_eq_S n).
1754 elim H1
1755   [apply (ex_intro ? ? a).split
1756     [rewrite > H2.
1757      rewrite > times_n_SO in ⊢ (? % ?).
1758      rewrite > sym_times.
1759      apply lt_times_l1
1760       [apply (divides_to_lt_O a n ? ?)
1761         [assumption
1762         |apply (witness a n (S (S O))).
1763          rewrite > sym_times.
1764          assumption
1765         ]
1766       |apply le_n
1767       ]
1768     |left.assumption
1769     ]
1770   |apply (ex_intro ? ? a).split
1771     [rewrite > H2.
1772      apply (le_to_lt_to_lt ? ((S(S O))*a))
1773       [rewrite > times_n_SO in ⊢ (? % ?).
1774        rewrite > sym_times.
1775        apply le_times_l.
1776        apply le_n_Sn
1777       |apply le_n
1778       ]
1779     |right.assumption
1780     ]
1781   ]
1782 qed.
1783
1784 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
1785 intro.simplify.reflexivity.
1786 qed.
1787
1788 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
1789 intros.reflexivity.
1790 qed.
1791
1792 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
1793 intro.simplify.rewrite < plus_n_Sm.reflexivity.
1794 qed.
1795
1796 theorem fact1: \forall n.
1797 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
1798 intro.elim n
1799   [rewrite < times_n_O.apply le_n
1800   |rewrite > times_SSO.
1801    rewrite > factS.
1802    rewrite > factS.
1803    rewrite < assoc_times.
1804    rewrite > factS.
1805    apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
1806     [apply le_times_l.
1807      rewrite > times_SSO.
1808      apply le_times_r.
1809      apply le_n_Sn
1810     |rewrite > assoc_times.
1811      rewrite > assoc_times.
1812      rewrite > assoc_times in ⊢ (? ? %).
1813      rewrite > exp_S.
1814      rewrite > assoc_times in ⊢ (? ? %).
1815      apply le_times_r.
1816      rewrite < assoc_times.
1817      rewrite < assoc_times.
1818      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
1819      rewrite > assoc_times.
1820      rewrite > assoc_times.
1821      rewrite > exp_S.
1822      rewrite > assoc_times in ⊢ (? ? %).
1823      apply le_times_r.
1824      rewrite > sym_times in ⊢ (? ? %).
1825      rewrite > assoc_times in ⊢ (? ? %).
1826      rewrite > assoc_times in ⊢ (? ? %).
1827      apply le_times_r.
1828      rewrite < assoc_times in ⊢ (? ? %).
1829      rewrite < assoc_times in ⊢ (? ? %).
1830      rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
1831      rewrite > assoc_times in ⊢ (? ? %).
1832      rewrite > assoc_times in ⊢ (? ? %).
1833      apply le_times_r.
1834      rewrite > sym_times in ⊢ (? ? (? ? %)).
1835      rewrite > sym_times in ⊢ (? ? %).
1836      assumption
1837     ]
1838   ]
1839 qed.
1840
1841 theorem monotonic_log: monotonic nat le log.
1842 unfold monotonic.intros.
1843 elim (le_to_or_lt_eq ? ? H) 0
1844   [cases x;intro
1845     [apply le_O_n
1846     |apply lt_S_to_le.
1847      apply (lt_exp_to_lt (S(S O)))
1848       [apply le_n
1849       |apply (le_to_lt_to_lt ? (S n))
1850         [apply le_exp_log.
1851          apply lt_O_S
1852         |apply (trans_lt ? y)
1853           [assumption
1854           |apply lt_exp_log
1855           ]
1856         ]
1857       ]
1858     ]
1859   |intro.rewrite < H1.apply le_n
1860   ]
1861 qed.
1862
1863 theorem lt_O_fact: \forall n. O < fact n.
1864 intro.elim n
1865   [simplify.apply lt_O_S
1866   |rewrite > factS.
1867    rewrite > (times_n_O O).
1868    apply lt_times
1869     [apply lt_O_S
1870     |assumption
1871     ]
1872   ]
1873 qed.
1874
1875 theorem fact2: \forall n.O < n \to
1876 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
1877 intros.elim H
1878   [simplify.apply le_S.apply le_n
1879   |rewrite > times_SSO.
1880    rewrite > factS.
1881    rewrite > factS.
1882    rewrite < assoc_times.
1883    rewrite > factS.
1884    rewrite < times_SSO in ⊢ (? ? %).
1885    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
1886     [rewrite > assoc_times in ⊢ (? ? %).
1887      rewrite > exp_S.
1888      rewrite > assoc_times.
1889      rewrite > assoc_times.
1890      rewrite > assoc_times.
1891      apply lt_times_r.
1892      rewrite > exp_S.
1893      rewrite > assoc_times.
1894      rewrite > sym_times in ⊢ (? ? %).
1895      rewrite > assoc_times in ⊢ (? ? %).
1896      rewrite > assoc_times in ⊢ (? ? %).
1897      apply lt_times_r.
1898      rewrite > sym_times.
1899      rewrite > assoc_times.
1900      rewrite > assoc_times.
1901      apply lt_times_r.
1902      rewrite < assoc_times.
1903      rewrite < assoc_times.
1904      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1905      rewrite > assoc_times.
1906      rewrite > assoc_times.
1907      rewrite > sym_times in ⊢ (? ? %).
1908      apply lt_times_r.
1909      rewrite < assoc_times.
1910      rewrite < sym_times.
1911      rewrite < assoc_times.
1912      assumption
1913     |apply lt_times_l1
1914       [rewrite > (times_n_O O) in ⊢ (? % ?).
1915        apply lt_times
1916         [rewrite > (times_n_O O) in ⊢ (? % ?).
1917          apply lt_times
1918           [apply lt_O_S
1919           |apply lt_O_S
1920           ]
1921         |apply lt_O_fact
1922         ]
1923       |apply le_n
1924       ]
1925     ]
1926   ]
1927 qed.
1928
1929 theorem lt_O_log: \forall n. S O < n \to O < log n.
1930 intros.elim H
1931   [simplify.apply lt_O_S
1932   |apply (lt_to_le_to_lt ? (log n1))
1933     [assumption
1934     |apply monotonic_log.
1935      apply le_n_Sn
1936     ]
1937   ]
1938 qed.
1939
1940 theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
1941 reflexivity.
1942 qed.
1943
1944 lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
1945 reflexivity.
1946 qed.
1947 (*
1948 theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
1949 reflexivity.
1950 qed.
1951 *)
1952 theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
1953 reflexivity.
1954 qed.
1955
1956 theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
1957 n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
1958 intros.
1959 elim H
1960   [rewrite > factS in ⊢ (? (? %) ?).
1961    rewrite > factS in ⊢ (? (? (? ? %)) ?).
1962    rewrite < assoc_times in ⊢ (? (? %) ?).
1963    rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
1964    rewrite > assoc_times in ⊢ (? (? %) ?).
1965    change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
1966
1967 theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
1968 intro.apply (nat_elim1 n).
1969 intros.
1970 elim (lt_O_to_or_eq_S m)
1971   [elim H2.clear H2.
1972    elim H4.clear H4.
1973    rewrite > H2.
1974    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1975     [apply monotonic_log.
1976      apply fact1
1977     |rewrite > assoc_times in ⊢ (? (? %) ?).
1978      rewrite > log_exp.
1979      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1980       [apply le_plus_r.
1981        apply log_times
1982       |rewrite > plus_n_Sm.
1983        rewrite > log_SSO.
1984        rewrite < times_n_Sm.
1985        apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
1986         [apply le_plus_r.
1987          apply le_plus_r.
1988          apply H.assumption
1989         |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
1990           [apply lt_plus_r.
1991            apply lt_plus_l.
1992            apply H.
1993            assumption.
1994           |rewrite > times_SSO_n.
1995            rewrite > distr_times_minus.
1996            rewrite > sym_plus.
1997            rewrite > plus_minus
1998             [rewrite > sym_plus.
1999              rewrite < assoc_times.
2000              apply le_n
2001             |rewrite < assoc_times.
2002              rewrite > times_n_SO in ⊢ (? % ?).
2003              apply le_times
2004               [apply le_n
2005               |apply lt_O_log.
2006                apply (lt_times_n_to_lt_r (S(S O)))
2007                 [apply lt_O_S
2008                 |rewrite < times_n_SO.
2009                  rewrite < H2.
2010                  assumption
2011                 ]
2012               ]
2013             ]
2014           ]
2015
2016              .
2017           ]
2018         |
2019            rewrite < eq_plus_minus_minus_plus.
2020
2021        rewrite > assoc_plus.
2022        apply lt_plus_r.
2023        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
2024        change with
2025         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
2026        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
2027         [apply le_S_S.
2028          apply lt_plus_r.
2029          apply lt_times_r.
2030          apply H.
2031          assumption
2032         |
2033
2034 theorem stirling: \forall n,k.k \le n \to
2035 log (fact n) < n*log n - n + k*log n.
2036 intro.
2037 apply (nat_elim1 n).
2038 intros.
2039 elim (lt_O_to_or_eq_S m)
2040   [elim H2.clear H2.
2041    elim H4.clear H4.
2042    rewrite > H2.
2043    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
2044     [apply monotonic_log.
2045      apply fact1
2046     |rewrite > assoc_times in ⊢ (? (? %) ?).
2047      rewrite > log_exp.
2048      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
2049       [apply le_plus_r.
2050        apply log_times
2051       |rewrite < plus_n_Sm.
2052        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
2053        change with
2054         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
2055        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
2056         [apply le_S_S.
2057          apply lt_plus_r.
2058          apply lt_times_r.
2059          apply H.
2060          assumption
2061         |
2062
2063           [
2064
2065        a*log a-a+k*log a
2066
2067 *)