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