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 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_A_SSO_A: \forall n.
1008 A((S(S O))*n) \le
1009  pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n.
1010 unfold A.intros.
1011 cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
1012   [rewrite > Hcut.
1013    rewrite < times_pi_p.
1014    apply le_pi_p.intros.
1015    lapply (prime_to_lt_SO ? (primeb_true_to_prime ? H1)) as H2.
1016    change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
1017    apply le_exp
1018     [apply lt_to_le.assumption
1019     |apply (trans_le ? (log i (i*n)))
1020       [apply le_log
1021         [assumption
1022         |apply not_le_to_lt.intro.
1023          apply (lt_to_not_le ? ? H).
1024          apply (trans_le ? (S O))
1025           [apply le_S_S.assumption
1026           |apply lt_to_le.assumption
1027           ]
1028         |apply le_times_l.
1029          assumption
1030         ]
1031       |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
1032        rewrite > log_exp
1033         [apply le_n
1034         |assumption
1035         |apply not_le_to_lt.intro.
1036          apply (lt_to_not_le ? ? H).
1037          apply (le_n_O_elim ? H3).
1038          apply lt_to_le.
1039          assumption
1040         ]
1041       ]
1042     ]
1043   |apply sym_eq.
1044    apply or_false_eq_SO_to_eq_pi_p
1045     [apply le_S_S.
1046      apply le_times_n.
1047      apply lt_O_S
1048     |intros.right.
1049      change with (exp i (log i n) = (exp i O)).
1050      apply eq_f.
1051      apply antisymmetric_le
1052       [cut (O < n)
1053         [apply le_S_S_to_le.
1054          apply (lt_exp_to_lt i)
1055           [apply (le_to_lt_to_lt ? n);assumption
1056           |apply (le_to_lt_to_lt ? n)
1057             [apply le_exp_log.
1058              assumption
1059             |rewrite < exp_n_SO.
1060              assumption
1061             ]
1062           ]
1063         |apply not_le_to_lt.intro.
1064          apply (lt_to_not_le ? ? H1).
1065          generalize in match H.
1066          apply (le_n_O_elim ? H2).
1067          intro.assumption
1068         ]
1069       |apply le_O_n
1070       ]
1071     ]
1072   ]
1073 qed.
1074
1075 (* so far so good
1076
1077 theorem le_A_BA: \forall n.
1078 A((S(S O))*n) \le B((S(S O))*n)*A n.
1079 (*
1080   [simplify.reflexivity
1081   |rewrite > times_SSO.
1082    rewrite > times_SSO.
1083    unfold A.
1084 apply (trans_le ? ((pi_p (S ((S(S O))*n)) primeb (λp:nat.p))*A n))
1085   [apply le_A_SSO_A
1086   |apply le_times_l.
1087    unfold B.
1088    apply le_pi_p.intros.
1089 *)
1090 intro.unfold A.unfold B.
1091 cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
1092   [rewrite > Hcut.
1093    rewrite < times_pi_p.
1094    apply le_pi_p.intros.
1095    apply le_trans i.
1096
1097
1098    change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
1099    apply le_exp
1100     [apply prime_to_lt_O.
1101      apply primeb_true_to_prime.
1102      assumption
1103     |apply (trans_le ? (log i (i*n)))
1104       [apply le_log
1105         [apply prime_to_lt_SO.
1106          apply primeb_true_to_prime.
1107          assumption
1108         |apply not_le_to_lt.intro.
1109          apply (lt_to_not_le ? ? H).
1110          apply (trans_le ? (S O))
1111           [apply le_S_S.assumption
1112           |apply prime_to_lt_O.
1113            apply primeb_true_to_prime.
1114            assumption
1115           ]
1116         |apply le_times_l.
1117          apply prime_to_lt_SO.
1118          apply primeb_true_to_prime.
1119          assumption
1120         ]
1121       |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
1122        rewrite > log_exp
1123         [apply le_n
1124         |apply prime_to_lt_SO.
1125          apply primeb_true_to_prime.
1126          assumption
1127         |apply not_le_to_lt.intro.
1128          apply (lt_to_not_le ? ? H).
1129          apply (le_n_O_elim ? H2).
1130          apply prime_to_lt_O.
1131          apply primeb_true_to_prime.
1132          assumption
1133         ]
1134       ]
1135     ]
1136   |apply sym_eq.
1137    apply or_false_eq_SO_to_eq_pi_p
1138     [apply le_S_S.
1139      apply le_times_n.
1140      apply lt_O_S
1141     |intros.right.
1142      change with (exp i (log i n) = (exp i O)).
1143      apply eq_f.
1144      apply antisymmetric_le
1145       [cut (O < n)
1146         [apply le_S_S_to_le.
1147          apply (lt_exp_to_lt i)
1148           [apply (le_to_lt_to_lt ? n);assumption
1149           |apply (le_to_lt_to_lt ? n)
1150             [apply le_exp_log.
1151              assumption
1152             |rewrite < exp_n_SO.
1153              assumption
1154             ]
1155           ]
1156         |apply not_le_to_lt.intro.
1157          apply (lt_to_not_le ? ? H1).
1158          generalize in match H.
1159          apply (le_n_O_elim ? H2).
1160          intro.assumption
1161         ]
1162       |apply le_O_n
1163       ]
1164     ]
1165   ]
1166 qed.
1167
1168
1169 unfold A.unfold B.
1170 rewrite > eq_A_A'.rewrite > eq_A_A'.
1171 unfold A'.unfold B.
1172
1173 (* da spostare *)
1174 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
1175 intros.elim p
1176   [reflexivity
1177   |simplify.autobatch
1178   ]
1179 qed.
1180
1181 theorem le_exp_log: \forall p,n. O < n \to
1182 exp p (
1183 log n) \le n.
1184 intros.
1185 apply leb_true_to_le.
1186 unfold log.
1187 apply (f_max_true (\lambda x.leb (exp p x) n)).
1188 apply (ex_intro ? ? O).
1189 split
1190   [apply le_O_n
1191   |apply le_to_leb_true.simplify.assumption
1192   ]
1193 qed.
1194
1195 theorem lt_log_n_n: \forall n. O < n \to log n < n.
1196 intros.
1197 cut (log n \le n)
1198   [elim (le_to_or_lt_eq ? ? Hcut)
1199     [assumption
1200     |absurd (exp (S(S O)) n \le n)
1201       [rewrite < H1 in ⊢ (? (? ? %) ?).
1202        apply le_exp_log.
1203        assumption
1204       |apply lt_to_not_le.
1205        apply lt_m_exp_nm.
1206        apply le_n
1207       ]
1208     ]
1209   |unfold log.apply le_max_n
1210   ]
1211 qed.
1212
1213 theorem le_log_n_n: \forall n. log n \le n.
1214 intro.
1215 cases n
1216   [apply le_n
1217   |apply lt_to_le.
1218    apply lt_log_n_n.
1219    apply lt_O_S
1220   ]
1221 qed.
1222
1223 theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
1224 intro.cases n
1225   [simplify.apply le_S.apply le_n
1226   |apply not_le_to_lt.
1227    apply leb_false_to_not_le.
1228    apply (lt_max_to_false ? (S n1) (S (log (S n1))))
1229     [apply le_S_S.apply le_n
1230     |apply lt_log_n_n.apply lt_O_S
1231     ]
1232   ]
1233 qed.
1234
1235 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
1236 (\forall m. p < m \to f m = false)
1237 \to max n f \le p.
1238 intros.
1239 apply not_lt_to_le.intro.
1240 apply not_eq_true_false.
1241 rewrite < (H1 ? H2).
1242 apply sym_eq.
1243 apply f_max_true.
1244 assumption.
1245 qed.
1246
1247 theorem log_times1: \forall n,m. O < n \to O < m \to
1248 log (n*m) \le S(log n+log m).
1249 intros.
1250 unfold in ⊢ (? (% ?) ?).
1251 apply f_false_to_le_max
1252   [apply (ex_intro ? ? O).
1253    split
1254     [apply le_O_n
1255     |apply le_to_leb_true.
1256      simplify.
1257      rewrite > times_n_SO.
1258      apply le_times;assumption
1259     ]
1260   |intros.
1261    apply lt_to_leb_false.
1262    apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
1263     [apply lt_times;apply lt_exp_log
1264     |rewrite < exp_plus_times.
1265      apply le_exp
1266       [apply lt_O_S
1267       |simplify.
1268        rewrite < plus_n_Sm.
1269        assumption
1270       ]
1271     ]
1272   ]
1273 qed.
1274
1275 theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
1276 intros.
1277 cases n
1278   [apply le_O_n
1279   |cases m
1280     [rewrite < times_n_O.
1281      apply le_O_n
1282     |apply log_times1;apply lt_O_S
1283     ]
1284   ]
1285 qed.
1286
1287 theorem log_exp: \forall n,m.O < m \to
1288 log ((exp (S(S O)) n)*m)=n+log m.
1289 intros.
1290 unfold log in ⊢ (? ? (% ?) ?).
1291 apply max_spec_to_max.
1292 unfold max_spec.
1293 split
1294   [split
1295     [elim n
1296       [simplify.
1297        rewrite < plus_n_O.
1298        apply le_log_n_n
1299       |simplify.
1300        rewrite < plus_n_O.
1301        rewrite > times_plus_l.
1302        apply (trans_le ? (S((S(S O))\sup(n1)*m)))
1303         [apply le_S_S.assumption
1304         |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
1305           [rewrite > (times_n_O O) in ⊢ (? % ?).
1306            apply lt_times
1307             [apply lt_O_exp.
1308              apply lt_O_S
1309             |assumption
1310             ]
1311           |intro.simplify.apply le_S_S.
1312            apply le_plus_n
1313           ]
1314         ]
1315       ]
1316     |simplify.
1317      apply le_to_leb_true.
1318      rewrite > exp_plus_times.
1319      apply le_times_r.
1320      apply le_exp_log.
1321      assumption
1322     ]
1323   |intros.
1324    simplify.
1325    apply lt_to_leb_false.
1326    apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
1327     [apply lt_times_r1
1328       [apply lt_O_exp.apply lt_O_S
1329       |apply lt_exp_log.
1330       ]
1331     |rewrite < exp_plus_times.
1332      apply le_exp
1333       [apply lt_O_S
1334       |rewrite < plus_n_Sm.
1335        assumption
1336       ]
1337     ]
1338   ]
1339 qed.
1340
1341 theorem log_SSO: \forall n. O < n \to
1342 log ((S(S O))*n) = S (log n).
1343 intros.
1344 change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
1345 rewrite > log_exp.reflexivity.assumption.
1346 qed.
1347
1348 theorem or_eq_S: \forall n.\exists m.
1349 (n = (S(S O))*m) \lor (n = S((S(S O))*m)).
1350 intro.
1351 elim n
1352   [apply (ex_intro ? ? O).left.apply times_n_O
1353   |elim H.elim H1
1354     [apply (ex_intro ? ? a).right.apply eq_f.assumption
1355     |apply (ex_intro ? ? (S a)).left.
1356      rewrite > H2.simplify.
1357      rewrite < plus_n_O.
1358      rewrite < plus_n_Sm.
1359      reflexivity
1360     ]
1361   ]
1362 qed.
1363
1364 theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
1365 ((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
1366 intros.
1367 elim (or_eq_S n).
1368 elim H1
1369   [apply (ex_intro ? ? a).split
1370     [rewrite > H2.
1371      rewrite > times_n_SO in ⊢ (? % ?).
1372      rewrite > sym_times.
1373      apply lt_times_l1
1374       [apply (divides_to_lt_O a n ? ?)
1375         [assumption
1376         |apply (witness a n (S (S O))).
1377          rewrite > sym_times.
1378          assumption
1379         ]
1380       |apply le_n
1381       ]
1382     |left.assumption
1383     ]
1384   |apply (ex_intro ? ? a).split
1385     [rewrite > H2.
1386      apply (le_to_lt_to_lt ? ((S(S O))*a))
1387       [rewrite > times_n_SO in ⊢ (? % ?).
1388        rewrite > sym_times.
1389        apply le_times_l.
1390        apply le_n_Sn
1391       |apply le_n
1392       ]
1393     |right.assumption
1394     ]
1395   ]
1396 qed.
1397
1398 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
1399 intro.simplify.reflexivity.
1400 qed.
1401
1402 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
1403 intros.reflexivity.
1404 qed.
1405
1406 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
1407 intro.simplify.rewrite < plus_n_Sm.reflexivity.
1408 qed.
1409
1410 theorem fact1: \forall n.
1411 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
1412 intro.elim n
1413   [rewrite < times_n_O.apply le_n
1414   |rewrite > times_SSO.
1415    rewrite > factS.
1416    rewrite > factS.
1417    rewrite < assoc_times.
1418    rewrite > factS.
1419    apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
1420     [apply le_times_l.
1421      rewrite > times_SSO.
1422      apply le_times_r.
1423      apply le_n_Sn
1424     |rewrite > assoc_times.
1425      rewrite > assoc_times.
1426      rewrite > assoc_times in ⊢ (? ? %).
1427      rewrite > exp_S.
1428      rewrite > assoc_times in ⊢ (? ? %).
1429      apply le_times_r.
1430      rewrite < assoc_times.
1431      rewrite < assoc_times.
1432      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
1433      rewrite > assoc_times.
1434      rewrite > assoc_times.
1435      rewrite > exp_S.
1436      rewrite > assoc_times in ⊢ (? ? %).
1437      apply le_times_r.
1438      rewrite > sym_times in ⊢ (? ? %).
1439      rewrite > assoc_times in ⊢ (? ? %).
1440      rewrite > assoc_times in ⊢ (? ? %).
1441      apply le_times_r.
1442      rewrite < assoc_times in ⊢ (? ? %).
1443      rewrite < assoc_times in ⊢ (? ? %).
1444      rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
1445      rewrite > assoc_times in ⊢ (? ? %).
1446      rewrite > assoc_times in ⊢ (? ? %).
1447      apply le_times_r.
1448      rewrite > sym_times in ⊢ (? ? (? ? %)).
1449      rewrite > sym_times in ⊢ (? ? %).
1450      assumption
1451     ]
1452   ]
1453 qed.
1454
1455 theorem monotonic_log: monotonic nat le log.
1456 unfold monotonic.intros.
1457 elim (le_to_or_lt_eq ? ? H) 0
1458   [cases x;intro
1459     [apply le_O_n
1460     |apply lt_S_to_le.
1461      apply (lt_exp_to_lt (S(S O)))
1462       [apply le_n
1463       |apply (le_to_lt_to_lt ? (S n))
1464         [apply le_exp_log.
1465          apply lt_O_S
1466         |apply (trans_lt ? y)
1467           [assumption
1468           |apply lt_exp_log
1469           ]
1470         ]
1471       ]
1472     ]
1473   |intro.rewrite < H1.apply le_n
1474   ]
1475 qed.
1476
1477 theorem lt_O_fact: \forall n. O < fact n.
1478 intro.elim n
1479   [simplify.apply lt_O_S
1480   |rewrite > factS.
1481    rewrite > (times_n_O O).
1482    apply lt_times
1483     [apply lt_O_S
1484     |assumption
1485     ]
1486   ]
1487 qed.
1488
1489 theorem fact2: \forall n.O < n \to
1490 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
1491 intros.elim H
1492   [simplify.apply le_S.apply le_n
1493   |rewrite > times_SSO.
1494    rewrite > factS.
1495    rewrite > factS.
1496    rewrite < assoc_times.
1497    rewrite > factS.
1498    rewrite < times_SSO in ⊢ (? ? %).
1499    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
1500     [rewrite > assoc_times in ⊢ (? ? %).
1501      rewrite > exp_S.
1502      rewrite > assoc_times.
1503      rewrite > assoc_times.
1504      rewrite > assoc_times.
1505      apply lt_times_r.
1506      rewrite > exp_S.
1507      rewrite > assoc_times.
1508      rewrite > sym_times in ⊢ (? ? %).
1509      rewrite > assoc_times in ⊢ (? ? %).
1510      rewrite > assoc_times in ⊢ (? ? %).
1511      apply lt_times_r.
1512      rewrite > sym_times.
1513      rewrite > assoc_times.
1514      rewrite > assoc_times.
1515      apply lt_times_r.
1516      rewrite < assoc_times.
1517      rewrite < assoc_times.
1518      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1519      rewrite > assoc_times.
1520      rewrite > assoc_times.
1521      rewrite > sym_times in ⊢ (? ? %).
1522      apply lt_times_r.
1523      rewrite < assoc_times.
1524      rewrite < sym_times.
1525      rewrite < assoc_times.
1526      assumption
1527     |apply lt_times_l1
1528       [rewrite > (times_n_O O) in ⊢ (? % ?).
1529        apply lt_times
1530         [rewrite > (times_n_O O) in ⊢ (? % ?).
1531          apply lt_times
1532           [apply lt_O_S
1533           |apply lt_O_S
1534           ]
1535         |apply lt_O_fact
1536         ]
1537       |apply le_n
1538       ]
1539     ]
1540   ]
1541 qed.
1542
1543 theorem lt_O_log: \forall n. S O < n \to O < log n.
1544 intros.elim H
1545   [simplify.apply lt_O_S
1546   |apply (lt_to_le_to_lt ? (log n1))
1547     [assumption
1548     |apply monotonic_log.
1549      apply le_n_Sn
1550     ]
1551   ]
1552 qed.
1553
1554 theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
1555 reflexivity.
1556 qed.
1557
1558 lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
1559 reflexivity.
1560 qed.
1561 (*
1562 theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
1563 reflexivity.
1564 qed.
1565 *)
1566 theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
1567 reflexivity.
1568 qed.
1569
1570 theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
1571 n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
1572 intros.
1573 elim H
1574   [rewrite > factS in ⊢ (? (? %) ?).
1575    rewrite > factS in ⊢ (? (? (? ? %)) ?).
1576    rewrite < assoc_times in ⊢ (? (? %) ?).
1577    rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
1578    rewrite > assoc_times in ⊢ (? (? %) ?).
1579    change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
1580
1581 theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
1582 intro.apply (nat_elim1 n).
1583 intros.
1584 elim (lt_O_to_or_eq_S m)
1585   [elim H2.clear H2.
1586    elim H4.clear H4.
1587    rewrite > H2.
1588    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1589     [apply monotonic_log.
1590      apply fact1
1591     |rewrite > assoc_times in ⊢ (? (? %) ?).
1592      rewrite > log_exp.
1593      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1594       [apply le_plus_r.
1595        apply log_times
1596       |rewrite > plus_n_Sm.
1597        rewrite > log_SSO.
1598        rewrite < times_n_Sm.
1599        apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
1600         [apply le_plus_r.
1601          apply le_plus_r.
1602          apply H.assumption
1603         |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
1604           [apply lt_plus_r.
1605            apply lt_plus_l.
1606            apply H.
1607            assumption.
1608           |rewrite > times_SSO_n.
1609            rewrite > distr_times_minus.
1610            rewrite > sym_plus.
1611            rewrite > plus_minus
1612             [rewrite > sym_plus.
1613              rewrite < assoc_times.
1614              apply le_n
1615             |rewrite < assoc_times.
1616              rewrite > times_n_SO in ⊢ (? % ?).
1617              apply le_times
1618               [apply le_n
1619               |apply lt_O_log.
1620                apply (lt_times_n_to_lt_r (S(S O)))
1621                 [apply lt_O_S
1622                 |rewrite < times_n_SO.
1623                  rewrite < H2.
1624                  assumption
1625                 ]
1626               ]
1627             ]
1628           ]
1629
1630              .
1631           ]
1632         |
1633            rewrite < eq_plus_minus_minus_plus.
1634
1635        rewrite > assoc_plus.
1636        apply lt_plus_r.
1637        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1638        change with
1639         (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)).
1640        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
1641         [apply le_S_S.
1642          apply lt_plus_r.
1643          apply lt_times_r.
1644          apply H.
1645          assumption
1646         |
1647
1648 theorem stirling: \forall n,k.k \le n \to
1649 log (fact n) < n*log n - n + k*log n.
1650 intro.
1651 apply (nat_elim1 n).
1652 intros.
1653 elim (lt_O_to_or_eq_S m)
1654   [elim H2.clear H2.
1655    elim H4.clear H4.
1656    rewrite > H2.
1657    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1658     [apply monotonic_log.
1659      apply fact1
1660     |rewrite > assoc_times in ⊢ (? (? %) ?).
1661      rewrite > log_exp.
1662      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1663       [apply le_plus_r.
1664        apply log_times
1665       |rewrite < plus_n_Sm.
1666        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1667        change with
1668         (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)).
1669        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
1670         [apply le_S_S.
1671          apply lt_plus_r.
1672          apply lt_times_r.
1673          apply H.
1674          assumption
1675         |
1676
1677           [
1678
1679        a*log a-a+k*log a
1680