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
  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 (* This is chebishev psi funcion *)
  26 definition A: nat \to nat \def
  27 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
  28
  29 theorem le_Al1: \forall n.
  30 A n \le pi_p (S n) primeb (\lambda p.n).
  31 intro.unfold A.
  32 cases n
  33   [simplify.apply le_n
  34   |apply le_pi_p.
  35    intros.
  36    apply le_exp_log.
  37    apply lt_O_S
  38   ]
  39 qed.
  40
  41 theorem le_Al: \forall n.
  42 A n \le exp n (prim n).
  43 intro.unfold prim.
  44 rewrite < exp_sigma_p.
  45 apply le_Al1.
  46 qed.
  47
  48 theorem leA_r2: \forall n.
  49 exp n (prim n) \le A n * A n.
  50 intro.unfold prim.
  51 elim (le_to_or_lt_eq ? ? (le_O_n n))
  52   [rewrite < (exp_sigma_p (S n) n primeb).
  53    unfold A.
  54    rewrite < times_pi_p.
  55    apply le_pi_p.
  56    intros.
  57    rewrite < exp_plus_times.
  58    apply (trans_le ? (exp i (S(log i n))))
  59     [apply lt_to_le.
  60      apply lt_exp_log.
  61      apply prime_to_lt_SO.
  62      apply primeb_true_to_prime.
  63      assumption
  64     |apply le_exp
  65       [apply prime_to_lt_O.
  66        apply primeb_true_to_prime.
  67        assumption
  68       |rewrite > plus_n_O.
  69        simplify.
  70        rewrite > plus_n_Sm.
  71        apply le_plus_r.
  72        apply lt_O_log
  73         [assumption
  74         |apply le_S_S_to_le.
  75          apply H1
  76         ]
  77       ]
  78     ]
  79   |rewrite < H. apply le_n
  80   ]
  81 qed.
  82
  83 (* an equivalent formulation for psi *)
  84 definition A': nat \to nat \def
  85 \lambda n. pi_p (S n) primeb
  86   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
  87
  88 theorem eq_A_A': \forall n.A n = A' n.
  89 intro.unfold A.unfold A'.
  90 apply eq_pi_p
  91   [intros.reflexivity
  92   |intros.
  93    apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
  94     [apply eq_f.apply sym_eq.apply sigma_p_true
  95     |apply sym_eq.apply exp_sigma_p
  96     ]
  97   ]
  98 qed.
  99
 100 theorem eq_pi_p_primeb_divides_b: \forall n,m.
 101 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
 102 = pi_p n primeb (\lambda p.exp p (ord m p)).
 103 intro.
 104 elim n
 105   [reflexivity
 106   |apply (bool_elim ? (primeb n1));intro
 107     [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
 108       [apply (bool_elim ? (divides_b n1 m));intro
 109         [rewrite > true_to_pi_p_Sn
 110           [apply eq_f.
 111            apply H
 112           |apply true_to_true_to_andb_true;assumption
 113           ]
 114         |rewrite > false_to_pi_p_Sn
 115           [rewrite > not_divides_to_ord_O
 116             [simplify in ⊢ (? ? ? (? % ?)).
 117              rewrite > sym_times.
 118              rewrite < times_n_SO.
 119              apply H
 120             |apply primeb_true_to_prime.assumption
 121             |apply divides_b_false_to_not_divides.
 122              assumption
 123             ]
 124           |rewrite > H1.rewrite > H2.reflexivity
 125           ]
 126         ]
 127       |assumption
 128       ]
 129     |rewrite > false_to_pi_p_Sn
 130       [rewrite > false_to_pi_p_Sn
 131         [apply H
 132         |assumption
 133         ]
 134       |rewrite > H1.reflexivity
 135       ]
 136     ]
 137   ]
 138 qed.
 139
 140 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
 141 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
 142 intro.elim q
 143   [apply False_ind.
 144    apply (not_le_Sn_O ? H1)
 145   |apply (bool_elim ? (primeb n∧divides_b n m));intro
 146     [rewrite > true_to_pi_p_Sn
 147       [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
 148         [apply eq_f.
 149          rewrite > (H (ord_rem m n))
 150           [apply eq_pi_p1
 151             [intros.
 152              apply (bool_elim ? (primeb x));intro
 153               [simplify.
 154                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
 155                 [apply sym_eq.
 156                  apply divides_to_divides_b_true
 157                   [apply prime_to_lt_O.
 158                    apply primeb_true_to_prime.
 159                    assumption
 160                   |apply (trans_divides ? (ord_rem m n))
 161                     [apply divides_b_true_to_divides.
 162                      assumption
 163                     |apply divides_ord_rem
 164                       [apply (trans_lt ? x)
 165                         [apply prime_to_lt_SO.
 166                          apply primeb_true_to_prime.
 167                          assumption
 168                         |assumption
 169                         ]
 170                       |assumption
 171                       ]
 172                     ]
 173                   ]
 174                 |apply sym_eq.
 175                  apply not_divides_to_divides_b_false
 176                   [apply prime_to_lt_O.
 177                    apply primeb_true_to_prime.
 178                    assumption
 179                   |apply ord_O_to_not_divides
 180                     [assumption
 181                     |apply primeb_true_to_prime.
 182                      assumption
 183                     |rewrite < (ord_ord_rem n)
 184                       [apply not_divides_to_ord_O
 185                         [apply primeb_true_to_prime.
 186                          assumption
 187                         |apply divides_b_false_to_not_divides.
 188                          assumption
 189                         ]
 190                       |assumption
 191                       |apply primeb_true_to_prime.
 192                        apply (andb_true_true ? ? H3)
 193                       |apply primeb_true_to_prime.
 194                        assumption
 195                       |assumption
 196                       ]
 197                     ]
 198                   ]
 199                 ]
 200               |reflexivity
 201               ]
 202             |intros.
 203              apply eq_f.
 204              apply ord_ord_rem
 205               [assumption
 206               |apply primeb_true_to_prime.
 207                apply (andb_true_true ? ? H3)
 208               |apply primeb_true_to_prime.
 209                apply (andb_true_true ? ? H5)
 210               |assumption
 211               ]
 212             ]
 213           |apply lt_O_ord_rem
 214             [apply prime_to_lt_SO.
 215              apply primeb_true_to_prime.
 216              apply (andb_true_true ? ? H3)
 217             |assumption
 218             ]
 219           |apply not_eq_to_le_to_lt
 220             [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
 221               [elim H4.
 222                intro.rewrite > H7 in H6.simplify in H6.
 223                apply (not_divides_ord_rem m n)
 224                 [assumption
 225                 |apply prime_to_lt_SO.
 226                  apply primeb_true_to_prime.
 227                  apply (andb_true_true ? ? H3)
 228                 |apply divides_b_true_to_divides.
 229                  apply (andb_true_true_r ? ? H6)
 230                 ]
 231               |elim H4.rewrite > H6.
 232                apply lt_to_not_eq.
 233                apply prime_to_lt_O.
 234                apply primeb_true_to_prime.
 235                apply (andb_true_true ? ? H3)
 236               ]
 237             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
 238               [apply le_to_le_max.
 239                apply divides_to_le
 240                 [assumption
 241                 |apply divides_ord_rem
 242                   [apply prime_to_lt_SO.
 243                    apply primeb_true_to_prime.
 244                    apply (andb_true_true ? ? H3)
 245                   |assumption
 246                   ]
 247                 ]
 248               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
 249                 [apply le_max_f_max_g.
 250                  intros.
 251                  apply (bool_elim ? (primeb i));intro
 252                   [simplify.
 253                    apply divides_to_divides_b_true
 254                     [apply prime_to_lt_O.
 255                      apply primeb_true_to_prime.
 256                      assumption
 257                     |apply (trans_divides ? (ord_rem m n))
 258                       [apply divides_b_true_to_divides.
 259                        apply (andb_true_true_r ? ? H5)
 260                       |apply divides_ord_rem
 261                         [apply prime_to_lt_SO.
 262                          apply primeb_true_to_prime.
 263                          apply (andb_true_true ? ? H3)
 264                         |assumption
 265                         ]
 266                       ]
 267                     ]
 268                   |rewrite > H6 in H5.
 269                    assumption
 270                   ]
 271                 |apply le_S_S_to_le.
 272                  assumption
 273                 ]
 274               ]
 275             ]
 276           ]
 277         |apply prime_to_lt_SO.
 278          apply primeb_true_to_prime.
 279          apply (andb_true_true ? ? H3)
 280         |assumption
 281         ]
 282       |assumption
 283       ]
 284     |elim (le_to_or_lt_eq ? ? H1)
 285       [rewrite > false_to_pi_p_Sn
 286         [apply H
 287           [assumption
 288           |apply false_to_lt_max
 289             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
 290               [apply lt_to_le.
 291                apply lt_SO_max_prime.
 292                assumption
 293               |apply le_S_S_to_le.
 294                assumption
 295               ]
 296             |assumption
 297             |apply le_S_S_to_le.
 298              assumption
 299             ]
 300           ]
 301         |assumption
 302         ]
 303       |rewrite < H4.
 304        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
 305        apply eq_pi_p
 306         [intros.
 307          apply (bool_elim ? (primeb x));intro
 308           [apply sym_eq.
 309            change with (divides_b x (S O) =false).
 310            apply not_divides_to_divides_b_false
 311             [apply prime_to_lt_O.
 312              apply primeb_true_to_prime.
 313              assumption
 314             |intro.
 315              apply (le_to_not_lt x (S O))
 316               [apply divides_to_le
 317                 [apply lt_O_S.assumption
 318                 |assumption
 319                 ]
 320               |elim (primeb_true_to_prime ? H6).
 321                assumption
 322               ]
 323             ]
 324           |reflexivity
 325           ]
 326         |intros.reflexivity
 327         ]
 328       ]
 329     ]
 330   ]
 331 qed.
 332
 333 (* factorization of n into primes *)
 334 theorem pi_p_primeb_divides_b: \forall n. O < n \to
 335 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 336 intros.
 337 apply lt_max_to_pi_p_primeb
 338   [assumption
 339   |apply le_S_S.
 340    apply le_max_n
 341   ]
 342 qed.
 343
 344 theorem pi_p_primeb: \forall n. O < n \to
 345 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
 346 intros.
 347 rewrite < eq_pi_p_primeb_divides_b.
 348 apply pi_p_primeb_divides_b.
 349 assumption.
 350 qed.
 351
 352 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
 353 ord n p \le log p n.
 354 intros.
 355 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
 356   [rewrite > log_exp
 357     [apply le_plus_n_r
 358     |assumption
 359     |apply lt_O_ord_rem;assumption
 360     ]
 361   |assumption
 362   |assumption
 363   ]
 364 qed.
 365
 366 theorem sigma_p_divides_b:
 367 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
 368 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 369 intro.elim m
 370   [reflexivity
 371   |simplify in ⊢ (? ? ? (? % ? ?)).
 372    rewrite > true_to_sigma_p_Sn
 373     [rewrite > sym_plus.rewrite < plus_n_SO.
 374      apply eq_f.
 375      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
 376      apply eq_sigma_p1
 377       [intros.
 378        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
 379         [apply sym_eq.
 380          apply divides_to_divides_b_true
 381           [apply lt_O_exp.
 382            apply prime_to_lt_O.
 383            assumption
 384           |apply (witness ? ? ((exp p (n - x))*n1)).
 385            rewrite < assoc_times.
 386            rewrite < exp_plus_times.
 387            apply eq_f2
 388             [apply eq_f.simplify.
 389              apply eq_f.
 390              rewrite > sym_plus.
 391              apply plus_minus_m_m.
 392              apply lt_to_le.assumption
 393             |reflexivity
 394             ]
 395           ]
 396         |apply sym_eq.
 397          apply False_ind.
 398          apply (divides_b_false_to_not_divides ? ? H5).
 399          apply (witness ? ? ((exp p (n - S x))*n1)).
 400          rewrite < assoc_times.
 401          rewrite < exp_plus_times.
 402          apply eq_f2
 403           [apply eq_f.
 404            rewrite > sym_plus.
 405            apply plus_minus_m_m.
 406            assumption
 407           |reflexivity
 408           ]
 409         ]
 410       |intros.reflexivity
 411       ]
 412     |apply divides_to_divides_b_true
 413       [apply lt_O_exp.
 414        apply prime_to_lt_O.assumption
 415       |apply (witness ? ? n1).reflexivity
 416       ]
 417     ]
 418   ]
 419 qed.
 420
 421 theorem sigma_p_divides_b1:
 422 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
 423 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 424 intros.
 425 lapply (prime_to_lt_SO ? H1) as H4.
 426 lapply (prime_to_lt_O ? H1) as H5.
 427 rewrite > (false_to_eq_sigma_p m k)
 428   [apply sigma_p_divides_b;assumption
 429   |assumption
 430   |intros.
 431    apply not_divides_to_divides_b_false
 432     [apply lt_O_exp.assumption
 433     |intro.apply (le_to_not_lt ? ? H6).
 434      unfold lt.
 435      rewrite < (ord_exp p)
 436       [rewrite > (plus_n_O m).
 437        rewrite < (not_divides_to_ord_O ? ? H1 H2).
 438        rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
 439        rewrite < ord_times
 440         [apply divides_to_le_ord
 441           [apply lt_O_exp.assumption
 442           |rewrite > (times_n_O O).
 443            apply lt_times
 444             [apply lt_O_exp.assumption
 445             |assumption
 446             ]
 447           |assumption
 448           |assumption
 449           ]
 450         |apply lt_O_exp.assumption
 451         |assumption
 452         |assumption
 453         ]
 454       |assumption
 455       ]
 456     ]
 457   ]
 458 qed.
 459
 460 theorem eq_ord_sigma_p:
 461 \forall n,m,x. O < n \to prime x \to
 462 exp x m \le n \to n < exp x (S m) \to
 463 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
 464 intros.
 465 lapply (prime_to_lt_SO ? H1).
 466 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
 467   [apply sigma_p_divides_b1
 468     [apply lt_O_ord_rem;assumption
 469     |assumption
 470     |apply not_divides_ord_rem;assumption
 471     |apply lt_S_to_le.
 472      apply (le_to_lt_to_lt ? (log x n))
 473       [apply le_ord_log;assumption
 474       |apply (lt_exp_to_lt x)
 475         [assumption
 476         |apply (le_to_lt_to_lt ? n ? ? H3).
 477          apply le_exp_log.
 478          assumption
 479         ]
 480       ]
 481     ]
 482   |assumption
 483   |assumption
 484   ]
 485 qed.
 486
 487 theorem pi_p_primeb1: \forall n. O < n \to
 488 n = pi_p (S n) primeb
 489   (\lambda p.(pi_p (log p n)
 490     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
 491 intros.
 492 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
 493 apply eq_pi_p1
 494   [intros.reflexivity
 495   |intros.
 496    rewrite > exp_sigma_p.
 497    apply eq_f.
 498    apply eq_ord_sigma_p
 499     [assumption
 500     |apply primeb_true_to_prime.
 501      assumption
 502     |apply le_exp_log.assumption
 503     |apply lt_exp_log.
 504      apply prime_to_lt_SO.
 505      apply primeb_true_to_prime.
 506      assumption
 507     ]
 508   ]
 509 qed.
 510
 511 (* the factorial function *)
 512 theorem eq_fact_pi_p:\forall n. fact n =
 513 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 514 intro.elim n
 515   [reflexivity
 516   |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
 517    rewrite > true_to_pi_p_Sn
 518     [apply eq_f.assumption
 519     |reflexivity
 520     ]
 521   ]
 522 qed.
 523
 524 theorem eq_sigma_p_div: \forall n,q.O < q \to
 525 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
 526 =n/q.
 527 intros.
 528 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 529   [apply div_mod_spec_intro
 530     [apply lt_mod_m_m.assumption
 531     |elim n
 532       [simplify.elim q;reflexivity
 533       |elim (or_div_mod1 n1 q)
 534         [elim H2.clear H2.
 535          rewrite > divides_to_mod_O
 536           [rewrite < plus_n_O.
 537            rewrite > true_to_sigma_p_Sn
 538             [rewrite > H4 in ⊢ (? ? % ?).
 539              apply eq_f2
 540               [rewrite < sym_plus.
 541                rewrite < plus_n_SO.
 542                apply eq_f.
 543                apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 544                 [apply div_mod_spec_div_mod.
 545                  assumption
 546                 |apply div_mod_spec_intro
 547                   [apply lt_mod_m_m.assumption
 548                   |assumption
 549                   ]
 550                 ]
 551               |reflexivity
 552               ]
 553             |apply true_to_true_to_andb_true
 554               [reflexivity
 555               |apply divides_to_divides_b_true;assumption
 556               ]
 557             ]
 558           |assumption
 559           |assumption
 560           ]
 561         |elim H2.clear H2.
 562          rewrite > false_to_sigma_p_Sn
 563           [rewrite > mod_S
 564             [rewrite < plus_n_Sm.
 565              apply eq_f.
 566              assumption
 567             |assumption
 568             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
 569               [assumption
 570               |apply False_ind.
 571                apply H3.
 572                apply (witness ? ? (S(div n1 q))).
 573                rewrite < times_n_Sm.
 574                rewrite < sym_plus.
 575                rewrite < H2 in ⊢ (? ? ? (? ? %)).
 576                rewrite > sym_times.
 577                assumption
 578               |apply lt_mod_m_m.
 579                assumption
 580               ]
 581             ]
 582           |rewrite > not_divides_to_divides_b_false
 583             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
 584             |assumption
 585             |assumption
 586             ]
 587           ]
 588         |assumption
 589         ]
 590       ]
 591     ]
 592   |apply div_mod_spec_div_mod.
 593    assumption
 594   ]
 595 qed.
 596
 597 (* still another characterization of the factorial *)
 598 theorem fact_pi_p: \forall n. fact n =
 599 pi_p (S n) primeb
 600   (\lambda p.(pi_p (log p n)
 601     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
 602 intros.
 603 rewrite > eq_fact_pi_p.
 604 apply (trans_eq ? ?
 605   (pi_p (S n) (λi:nat.leb (S O) i)
 606    (λn.pi_p (S n) primeb
 607     (\lambda p.(pi_p (log p n)
 608      (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
 609   [apply eq_pi_p1;intros
 610     [reflexivity
 611     |apply pi_p_primeb1.
 612      apply leb_true_to_le.assumption
 613     ]
 614   |apply (trans_eq ? ?
 615     (pi_p (S n) (λi:nat.leb (S O) i)
 616      (λn:nat
 617       .pi_p (S n) (\lambda p.primeb p\land leb p n)
 618        (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
 619     [apply eq_pi_p1
 620       [intros.reflexivity
 621       |intros.apply eq_pi_p1
 622         [intros.elim (primeb x1)
 623           [simplify.apply sym_eq.
 624            apply le_to_leb_true.
 625            apply le_S_S_to_le.
 626            assumption
 627           |reflexivity
 628           ]
 629         |intros.reflexivity
 630         ]
 631       ]
 632     |apply (trans_eq ? ?
 633       (pi_p (S n) (λi:nat.leb (S O) i)
 634        (λm:nat
 635         .pi_p (S n) (λp:nat.primeb p∧leb p m)
 636          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
 637       [apply eq_pi_p1
 638         [intros.reflexivity
 639         |intros.
 640          apply sym_eq.
 641          apply false_to_eq_pi_p
 642           [assumption
 643           |intros.rewrite > lt_to_leb_false
 644             [elim primeb;reflexivity|assumption]
 645           ]
 646         ]
 647       |(* make a general theorem *)
 648        apply (trans_eq ? ?
 649         (pi_p (S n) primeb
 650          (λp:nat
 651           .pi_p (S n) (λm.leb p m)
 652            (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
 653         ))
 654         [apply pi_p_pi_p1.
 655          intros.
 656          apply (bool_elim ? (primeb y \land leb y x));intros
 657           [rewrite > (le_to_leb_true (S O) x)
 658             [reflexivity
 659             |apply (trans_le ? y)
 660               [apply prime_to_lt_O.
 661                apply primeb_true_to_prime.
 662                apply (andb_true_true ? ? H2)
 663               |apply leb_true_to_le.
 664                apply (andb_true_true_r ? ? H2)
 665               ]
 666             ]
 667           |elim (leb (S O) x);reflexivity
 668           ]
 669         |apply eq_pi_p1
 670           [intros.reflexivity
 671           |intros.
 672            apply (trans_eq ? ?
 673             (pi_p (S n) (λm:nat.leb x m)
 674              (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
 675             [apply eq_pi_p1
 676               [intros.reflexivity
 677               |intros.
 678                apply sym_eq.
 679                apply false_to_eq_pi_p
 680                 [apply le_log
 681                   [apply prime_to_lt_SO.
 682                    apply primeb_true_to_prime.
 683                    assumption
 684                   |apply le_S_S_to_le.
 685                    assumption
 686                   ]
 687                 |intros.
 688                  apply not_divides_to_divides_b_false
 689                   [apply lt_O_exp.
 690                    apply prime_to_lt_O.
 691                    apply primeb_true_to_prime.
 692                    assumption
 693                   |intro.
 694                    apply (lt_to_not_le x1 (exp x (S i)))
 695                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
 696                       [apply lt_exp_log.
 697                        apply prime_to_lt_SO.
 698                        apply primeb_true_to_prime.
 699                        assumption
 700                       |apply le_exp
 701                         [apply prime_to_lt_O.
 702                          apply primeb_true_to_prime.
 703                          assumption
 704                         |apply le_S_S.
 705                          assumption
 706                         ]
 707                       ]
 708                     |apply divides_to_le
 709                       [apply (lt_to_le_to_lt ? x)
 710                         [apply prime_to_lt_O.
 711                          apply primeb_true_to_prime.
 712                          assumption
 713                         |apply leb_true_to_le.
 714                          assumption
 715                         ]
 716                       |assumption
 717                       ]
 718                     ]
 719                   ]
 720                 ]
 721               ]
 722             |apply
 723              (trans_eq ? ?
 724               (pi_p (log x n) (λi:nat.true)
 725                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
 726               [apply (pi_p_pi_p1 (\lambda m,i.x)).
 727                intros.
 728                reflexivity
 729               |apply eq_pi_p1
 730                 [intros.reflexivity
 731                 |intros.
 732                  rewrite > exp_sigma_p.
 733                  apply eq_f.
 734                  apply (trans_eq ? ?
 735                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
 736                   [apply eq_sigma_p1
 737                     [intros.
 738                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
 739                       [apply (bool_elim ? (leb x x2));intro
 740                         [rewrite > le_to_leb_true
 741                           [reflexivity
 742                           |apply (trans_le ? x)
 743                             [apply prime_to_lt_O.
 744                              apply primeb_true_to_prime.
 745                              assumption
 746                             |apply leb_true_to_le.
 747                              assumption
 748                             ]
 749                           ]
 750                         |rewrite > lt_to_leb_false
 751                           [reflexivity
 752                           |apply not_le_to_lt.intro.
 753                            apply (leb_false_to_not_le ? ? H6).
 754                            apply (trans_le ? (exp x (S x1)))
 755                             [rewrite > times_n_SO in ⊢ (? % ?).
 756                              change with (exp x (S O) \le exp x (S x1)).
 757                              apply le_exp
 758                               [apply prime_to_lt_O.
 759                                apply primeb_true_to_prime.
 760                                assumption
 761                               |apply le_S_S.apply le_O_n.
 762                               ]
 763                             |apply divides_to_le
 764                               [assumption
 765                               |apply divides_b_true_to_divides.
 766                                assumption
 767                               ]
 768                             ]
 769                           ]
 770                         ]
 771                       |rewrite < andb_sym.
 772                        rewrite < andb_sym in ⊢ (? ? ? %).
 773                        reflexivity
 774                       ]
 775                     |intros.reflexivity
 776                     ]
 777                   |apply eq_sigma_p_div.
 778                    apply lt_O_exp.
 779                    apply prime_to_lt_O.
 780                    apply primeb_true_to_prime.
 781                    assumption
 782                   ]
 783                 ]
 784               ]
 785             ]
 786           ]
 787         ]
 788       ]
 789     ]
 790   ]
 791 qed.
 792
 793 (* odd n is just mod n (S(S O))
 794 let rec odd n \def
 795   match n with
 796   [ O \Rightarrow O
 797   | S m \Rightarrow (S O) - odd m
 798   ].
 799
 800 theorem le_odd_SO: \forall n. odd n \le S O.
 801 intro.elim n
 802   [apply le_O_n
 803   |simplify.cases (odd n1)
 804     [simplify.apply le_n.
 805     |apply le_O_n
 806     ]
 807   ]
 808 qed.
 809
 810 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
 811 intro.elim n
 812   [apply (lt_O_n_elim ? H).
 813    intro.simplify.reflexivity
 814   |
 815 *)
 816
 817 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
 818 pi_p (S ((S(S O))*n)) primeb
 819   (\lambda p.(pi_p (log p ((S(S O))*n))
 820     (\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)))))))).
 821 intros.rewrite > fact_pi_p.
 822 apply eq_pi_p1
 823   [intros.reflexivity
 824   |intros.apply eq_pi_p
 825     [intros.reflexivity
 826     |intros.
 827      rewrite < exp_plus_times.
 828      apply eq_f.
 829      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 830      apply SSO_mod.
 831      apply lt_O_exp.
 832      apply prime_to_lt_O.
 833      apply primeb_true_to_prime.
 834      assumption
 835     ]
 836   ]
 837 qed.
 838
 839 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
 840 pi_p (S ((S(S O))*n)) primeb
 841   (\lambda p.(pi_p (log p ((S(S O))*n))
 842     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
 843 pi_p (S ((S(S O))*n)) primeb
 844   (\lambda p.(pi_p (log p ((S(S O))*n))
 845     (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
 846 intros.
 847 rewrite < times_pi_p.
 848 rewrite > fact_pi_p2.
 849 apply eq_pi_p;intros
 850   [reflexivity
 851   |apply times_pi_p
 852   ]
 853 qed.
 854
 855 theorem pi_p_primeb4: \forall n. S O < n \to
 856 pi_p (S ((S(S O))*n)) primeb
 857   (\lambda p.(pi_p (log p ((S(S O))*n))
 858     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 859 =
 860 pi_p (S n) primeb
 861   (\lambda p.(pi_p (log p (S(S O)*n))
 862     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 863 intros.
 864 apply or_false_eq_SO_to_eq_pi_p
 865   [apply le_S_S.
 866    apply le_times_n.
 867    apply lt_O_S
 868   |intros.
 869    right.
 870    rewrite > log_i_SSOn
 871     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
 872      rewrite < times_n_SO.
 873      rewrite > eq_div_O
 874       [reflexivity
 875       |simplify.rewrite < times_n_SO.assumption
 876       ]
 877     |assumption
 878     |assumption
 879     |apply le_S_S_to_le.assumption
 880     ]
 881   ]
 882 qed.
 883
 884 theorem pi_p_primeb5: \forall n. S O < n \to
 885 pi_p (S ((S(S O))*n)) primeb
 886   (\lambda p.(pi_p (log p ((S(S O))*n))
 887     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 888 =
 889 pi_p (S n) primeb
 890   (\lambda p.(pi_p (log p n)
 891     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 892 intros.
 893 rewrite > (pi_p_primeb4 ? H).
 894 apply eq_pi_p1;intros
 895   [reflexivity
 896   |apply or_false_eq_SO_to_eq_pi_p
 897     [apply le_log
 898       [apply prime_to_lt_SO.
 899        apply primeb_true_to_prime.
 900        assumption
 901       |apply le_times_n.
 902        apply lt_O_S
 903       ]
 904     |intros.right.
 905      rewrite > eq_div_O
 906       [simplify.reflexivity
 907       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
 908         [apply lt_exp_log.
 909          apply prime_to_lt_SO.
 910          apply primeb_true_to_prime.
 911          assumption
 912         |apply le_exp
 913           [apply prime_to_lt_O.
 914            apply primeb_true_to_prime.
 915            assumption
 916           |apply le_S_S.
 917            assumption
 918           ]
 919         ]
 920       ]
 921     ]
 922   ]
 923 qed.
 924
 925 theorem exp_fact_SSO: \forall n.
 926 exp (fact n) (S(S O))
 927 =
 928 pi_p (S n) primeb
 929   (\lambda p.(pi_p (log p n)
 930     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 931 intros.
 932 rewrite > fact_pi_p.
 933 rewrite < exp_pi_p.
 934 apply eq_pi_p;intros
 935   [reflexivity
 936   |apply sym_eq.
 937    apply exp_times_pi_p
 938   ]
 939 qed.
 940
 941 definition B \def
 942 \lambda n.
 943 pi_p (S n) primeb
 944   (\lambda p.(pi_p (log p n)
 945     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 946
 947 theorem eq_fact_B:\forall n.S O < n \to
 948 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 949 intros. unfold B.
 950 rewrite > fact_pi_p3.
 951 apply eq_f2
 952   [apply sym_eq.
 953    rewrite > pi_p_primeb5
 954     [apply exp_fact_SSO
 955     |assumption
 956     ]
 957   |reflexivity
 958   ]
 959 qed.
 960
 961 theorem le_B_A: \forall n. B n \le A n.
 962 intro.unfold B.
 963 rewrite > eq_A_A'.
 964 unfold A'.
 965 apply le_pi_p.intros.
 966 apply le_pi_p.intros.
 967 rewrite > exp_n_SO in ⊢ (? ? %).
 968 apply le_exp
 969   [apply prime_to_lt_O.
 970    apply primeb_true_to_prime.
 971    assumption
 972   |apply le_S_S_to_le.
 973    apply lt_mod_m_m.
 974    apply lt_O_S
 975   ]
 976 qed.
 977
 978 theorem le_fact_A:\forall n.S O < n \to
 979 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
 980 intros.
 981 rewrite > eq_fact_B
 982   [apply le_times_r.
 983    apply le_B_A
 984   |assumption
 985   ]
 986 qed.
 987
 988 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 989 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
 990 intros.
 991 apply (le_times_to_le (exp (fact n) (S(S O))))
 992   [apply lt_O_exp.
 993    apply lt_O_fact
 994   |rewrite < eq_fact_B
 995     [rewrite < sym_times in ⊢ (? ? %).
 996      rewrite > exp_SSO.
 997      rewrite < assoc_times.
 998      apply fact1
 999     |assumption
1000     ]
1001   ]
1002 qed.
1003
1004 theorem le_B_exp: \forall n.
1005 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1006 intro.cases n
1007   [apply le_n
1008   |cases n1
1009     [simplify.apply le_S.apply le_S.apply le_n
1010     |apply lt_SO_to_le_B_exp.
1011      apply le_S_S.apply lt_O_S.
1012     ]
1013   ]
1014 qed.
1015
1016 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1017 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1018 intros.
1019 apply (le_times_to_le (exp (fact n) (S(S O))))
1020   [apply lt_O_exp.
1021    apply lt_O_fact
1022   |rewrite < assoc_times in ⊢ (? ? %).
1023    rewrite > sym_times in ⊢ (? ? (? % ?)).
1024    rewrite > assoc_times in ⊢ (? ? %).
1025    rewrite < eq_fact_B
1026     [rewrite < sym_times.
1027      apply fact3.
1028      apply lt_to_le.assumption
1029     |assumption
1030     ]
1031   ]
1032 qed.
1033
1034 theorem le_exp_B: \forall n. O < n \to
1035 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1036 intros.
1037 elim H
1038   [apply le_n
1039   |apply lt_SO_to_le_exp_B.
1040    apply le_S_S.assumption
1041   ]
1042 qed.
1043
1044 theorem eq_A_SSO_n: \forall n.O < n \to
1045 A((S(S O))*n) =
1046  pi_p (S ((S(S O))*n)) primeb
1047   (\lambda p.(pi_p (log p ((S(S O))*n) )
1048     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1049  *A n.
1050 intro.
1051 rewrite > eq_A_A'.rewrite > eq_A_A'.
1052 unfold A'.intros.
1053 cut (
1054  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1055  = pi_p (S ((S(S O))*n)) primeb
1056     (λ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))))))))
1057   [rewrite > Hcut.
1058    rewrite < times_pi_p.
1059    apply eq_pi_p1;intros
1060     [reflexivity
1061     |rewrite < times_pi_p.
1062      apply eq_pi_p;intros
1063       [reflexivity
1064       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1065         [simplify.rewrite < times_n_SO.apply times_n_SO
1066         |simplify.rewrite < plus_n_O.apply times_n_SO
1067         ]
1068       ]
1069     ]
1070   |apply (trans_eq ? ? (pi_p (S n) primeb
1071     (\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))))))))
1072     [apply eq_pi_p1;intros
1073       [reflexivity
1074       |apply eq_pi_p1;intros
1075         [reflexivity
1076         |rewrite > lt_to_leb_false
1077           [simplify.apply times_n_SO
1078           |apply le_S_S.
1079            apply (trans_le ? (exp x (log x n)))
1080             [apply le_exp
1081               [apply prime_to_lt_O.
1082                apply primeb_true_to_prime.
1083                assumption
1084               |assumption
1085               ]
1086             |apply le_exp_log.
1087              assumption
1088             ]
1089           ]
1090         ]
1091       ]
1092     |apply (trans_eq ? ?
1093       (pi_p (S ((S(S O))*n)) primeb
1094        (λp:nat.pi_p (log p n) (λi:nat.true)
1095         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1096       [apply sym_eq.
1097        apply or_false_eq_SO_to_eq_pi_p
1098         [apply le_S_S.
1099          simplify.
1100          apply le_plus_n_r
1101         |intros.right.
1102          rewrite > lt_to_log_O
1103           [reflexivity
1104           |assumption
1105           |assumption
1106           ]
1107         ]
1108       |apply eq_pi_p1;intros
1109         [reflexivity
1110         |apply sym_eq.
1111          apply or_false_eq_SO_to_eq_pi_p
1112           [apply le_log
1113             [apply prime_to_lt_SO.
1114              apply primeb_true_to_prime.
1115              assumption
1116             |simplify.
1117              apply le_plus_n_r
1118             ]
1119           |intros.right.
1120            rewrite > le_to_leb_true
1121             [simplify.reflexivity
1122             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1123               [apply lt_exp_log.
1124                apply prime_to_lt_SO.
1125                apply primeb_true_to_prime.
1126                assumption
1127               |apply le_exp
1128                 [apply prime_to_lt_O.
1129                  apply primeb_true_to_prime.
1130                  assumption
1131                 |apply le_S_S.assumption
1132                 ]
1133               ]
1134             ]
1135           ]
1136         ]
1137       ]
1138     ]
1139   ]
1140 qed.
1141
1142 theorem le_A_BA1: \forall n. O < n \to
1143 A((S(S O))*n) \le B((S(S O))*n)*A n.
1144 intros.
1145 rewrite > eq_A_SSO_n
1146   [apply le_times_l.
1147    unfold B.
1148    apply le_pi_p.intros.
1149    apply le_pi_p.intros.
1150    apply le_exp
1151     [apply prime_to_lt_O.
1152      apply primeb_true_to_prime.
1153      assumption
1154     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1155       [simplify in ⊢ (? % ?).
1156        cut ((S(S O))*n/i\sup(S i1) = S O)
1157         [rewrite > Hcut.apply le_n
1158         |apply (div_mod_spec_to_eq
1159           ((S(S O))*n) (exp i (S i1))
1160            ? (mod ((S(S O))*n) (exp i (S i1)))
1161            ? (minus ((S(S O))*n) (exp i (S i1))) )
1162           [apply div_mod_spec_div_mod.
1163            apply lt_O_exp.
1164            apply prime_to_lt_O.
1165            apply primeb_true_to_prime.
1166            assumption
1167           |cut (i\sup(S i1)≤(S(S O))*n)
1168             [apply div_mod_spec_intro
1169               [apply lt_plus_to_lt_minus
1170                 [assumption
1171                 |simplify in ⊢ (? % ?).
1172                  rewrite < plus_n_O.
1173                  apply lt_plus
1174                   [apply leb_true_to_le.assumption
1175                   |apply leb_true_to_le.assumption
1176                   ]
1177                 ]
1178               |rewrite > sym_plus.
1179                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1180                rewrite < times_n_SO.
1181                apply plus_minus_m_m.
1182                assumption
1183               ]
1184             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1185               [apply le_exp
1186                 [apply prime_to_lt_O.
1187                  apply primeb_true_to_prime.
1188                  assumption
1189                 |assumption
1190                 ]
1191               |apply le_exp_log.
1192                rewrite > (times_n_O O) in ⊢ (? % ?).
1193                apply lt_times
1194                 [apply lt_O_S
1195                 |assumption
1196                 ]
1197               ]
1198             ]
1199           ]
1200         ]
1201       |apply le_O_n
1202       ]
1203     ]
1204   |assumption
1205   ]
1206 qed.
1207
1208 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1209 intros.cases n
1210   [apply le_n
1211   |apply le_A_BA1.apply lt_O_S
1212   ]
1213 qed.
1214
1215 theorem le_A_exp: \forall n.
1216 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1217 intro.
1218 apply (trans_le ? (B((S(S O))*n)*A n))
1219   [apply le_A_BA
1220   |apply le_times_l.
1221    apply le_B_exp
1222   ]
1223 qed.
1224
1225 theorem le_A_exp1: \forall n.
1226 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1227 intro.elim n
1228   [simplify.apply le_S_S.apply le_O_n
1229   |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1230    apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1231     [apply le_A_exp
1232     |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
1233       [apply le_times_r.
1234        assumption
1235       |rewrite < exp_plus_times.
1236        simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1237        apply le_n
1238       ]
1239     ]
1240   ]
1241 qed.
1242
1243 theorem monotonic_A: monotonic nat le A.
1244 unfold.intros.
1245 elim H
1246   [apply le_n
1247   |apply (trans_le ? (A n1))
1248     [assumption
1249     |unfold A.
1250      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1251           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1252       [apply (bool_elim ? (primeb (S n1)));intro
1253         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1254          rewrite > times_n_SO in ⊢ (? % ?).
1255          rewrite > sym_times.
1256          apply le_times
1257           [apply lt_O_exp.apply lt_O_S
1258           |assumption
1259           ]
1260         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1261          assumption
1262         ]
1263       |apply le_pi_p.intros.
1264        apply le_exp
1265         [apply prime_to_lt_O.
1266          apply primeb_true_to_prime.
1267          assumption
1268         |apply le_log
1269           [apply prime_to_lt_SO.
1270            apply primeb_true_to_prime.
1271            assumption
1272           |apply le_S.apply le_n
1273           ]
1274         ]
1275       ]
1276     ]
1277   ]
1278 qed.
1279
1280 theorem le_A_exp2: \forall n. O < n \to
1281 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1282 intros.
1283 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1284   [apply monotonic_A.
1285    apply lt_to_le.
1286    apply lt_exp_log.
1287    apply le_n
1288   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1289     [apply le_A_exp1
1290     |apply le_exp
1291       [apply lt_O_S
1292       |rewrite > assoc_times.apply le_times_r.
1293        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1294        apply le_times_r.
1295        apply le_exp_log.
1296        assumption
1297       ]
1298     ]
1299   ]
1300 qed.
1301
1302 (* example *)
1303 theorem A_SO: A (S O) = S O.
1304 reflexivity.
1305 qed.
1306
1307 theorem A_SSO: A (S(S O)) = S (S O).
1308 reflexivity.
1309 qed.
1310
1311 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1312 reflexivity.
1313 qed.
1314
1315 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1316 reflexivity.
1317 qed.
1318
1319 (* da spostare *)
1320 theorem or_eq_eq_S: \forall n.\exists m.
1321 n = (S(S O))*m \lor n = S ((S(S O))*m).
1322 intro.elim n
1323   [apply (ex_intro ? ? O).
1324    left.reflexivity
1325   |elim H.elim H1
1326     [apply (ex_intro ? ? a).
1327      right.apply eq_f.assumption
1328     |apply (ex_intro ? ? (S a)).
1329      left.rewrite > H2.
1330      apply sym_eq.
1331      apply times_SSO
1332     ]
1333   ]
1334 qed.
1335
1336 (* a better result *)
1337 theorem le_A_exp3: \forall n. S O < n \to
1338 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1339 intro.
1340 apply (nat_elim1 n).
1341 intros.
1342 elim (or_eq_eq_S m).
1343 elim H2
1344   [elim (le_to_or_lt_eq (S O) a)
1345     [rewrite > H3 in ⊢ (? % ?).
1346      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1347       [apply le_A_exp
1348       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1349          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1350         [apply le_times_r.
1351          apply H
1352           [rewrite > H3.
1353            rewrite > times_n_SO in ⊢ (? % ?).
1354            rewrite > sym_times.
1355            apply lt_times_l1
1356             [apply lt_to_le.assumption
1357             |apply le_n
1358             ]
1359           |assumption
1360           ]
1361         |rewrite > sym_times.
1362          rewrite > assoc_times.
1363          rewrite < exp_plus_times.
1364          apply (trans_le ?
1365           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1366           [rewrite > assoc_times.
1367            apply le_times_r.
1368            rewrite < exp_plus_times.
1369            apply le_exp
1370             [apply lt_O_S
1371             |rewrite < H3.
1372              simplify.
1373              rewrite < plus_n_O.
1374              apply le_S.apply le_S.
1375              apply le_n
1376             ]
1377           |apply le_times_l.
1378            rewrite > times_exp.
1379            apply monotonic_exp1.
1380            rewrite > H3.
1381            rewrite > sym_times.
1382            cases a
1383             [apply le_n
1384             |simplify.
1385              rewrite < plus_n_Sm.
1386              apply le_S.
1387              apply le_n
1388             ]
1389           ]
1390         ]
1391       ]
1392     |rewrite < H4 in H3.
1393      simplify in H3.
1394      rewrite > H3.
1395      simplify.
1396      apply le_S_S.apply le_S_S.apply le_O_n
1397     |apply not_lt_to_le.intro.
1398      apply (lt_to_not_le ? ? H1).
1399      rewrite > H3.
1400      apply (le_n_O_elim a)
1401       [apply le_S_S_to_le.assumption
1402       |apply le_O_n
1403       ]
1404     ]
1405   |elim (le_to_or_lt_eq O a (le_O_n ?))
1406     [apply (trans_le ? (A ((S(S O))*(S a))))
1407       [apply monotonic_A.
1408        rewrite > H3.
1409        rewrite > times_SSO.
1410        apply le_n_Sn
1411       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1412         [apply le_A_exp
1413         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1414            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1415           [apply le_times_r.
1416            apply H
1417             [rewrite > H3.
1418              apply le_S_S.
1419              simplify.
1420              rewrite > plus_n_SO.
1421              apply le_plus_r.
1422              rewrite < plus_n_O.
1423              assumption
1424             |apply le_S_S.assumption
1425             ]
1426           |rewrite > sym_times.
1427            rewrite > assoc_times.
1428            rewrite < exp_plus_times.
1429            apply (trans_le ?
1430             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1431             [rewrite > assoc_times.
1432              apply le_times_r.
1433              rewrite < exp_plus_times.
1434              apply le_exp
1435               [apply lt_O_S
1436               |rewrite > times_SSO.
1437                rewrite < H3.
1438                simplify.
1439                rewrite < plus_n_Sm.
1440                rewrite < plus_n_O.
1441                apply le_n
1442               ]
1443             |apply le_times_l.
1444              rewrite > times_exp.
1445              apply monotonic_exp1.
1446              rewrite > H3.
1447              rewrite > sym_times.
1448              apply le_n
1449             ]
1450           ]
1451         ]
1452       ]
1453     |rewrite < H4 in H3.simplify in H3.
1454      apply False_ind.
1455      apply (lt_to_not_le ? ? H1).
1456      rewrite > H3.
1457      apply le_n
1458     ]
1459   ]
1460 qed.
1461
1462 theorem eq_sigma_pi_SO_n: \forall n.
1463 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1464 intro.elim n
1465   [reflexivity
1466   |rewrite > true_to_sigma_p_Sn
1467     [rewrite > H.reflexivity
1468     |reflexivity
1469     ]
1470   ]
1471 qed.
1472
1473 theorem leA_prim: \forall n.
1474 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1475 intro.
1476 unfold prim.
1477 rewrite < (exp_sigma_p (S n) n primeb).
1478 unfold A.
1479 rewrite < times_pi_p.
1480 apply le_pi_p.
1481 intros.
1482 rewrite > sym_times.
1483 change in ⊢ (? ? %) with (exp i (S (log i n))).
1484 apply lt_to_le.
1485 apply lt_exp_log.
1486 apply prime_to_lt_SO.
1487 apply primeb_true_to_prime.
1488 assumption.
1489 qed.
1490
1491
1492 (* the inequalities *)
1493 theorem le_exp_priml: \forall n. O < n \to
1494 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1495 intros.
1496 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1497   [apply le_exp_B.assumption
1498   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1499    apply le_times_r.
1500    apply (trans_le ? (A ((S(S O))*n)))
1501     [apply le_B_A
1502     |apply le_Al
1503     ]
1504   ]
1505 qed.
1506
1507 theorem le_priml: \forall n. O < n \to
1508 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1509 intros.
1510 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1511   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1512     [apply le_log
1513       [apply le_n
1514       |apply le_exp_priml.assumption
1515       ]
1516     |rewrite > sym_times in ⊢ (? ? %).
1517      apply log_exp1.
1518      apply le_n
1519     ]
1520   |apply le_n
1521   ]
1522 qed.
1523
1524 theorem le_exp_primr: \forall n. S O < n \to
1525 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
1526 intros.
1527 apply (trans_le ? (exp (A n) (S(S O))))
1528   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1529    rewrite < times_n_SO.
1530    apply leA_r2
1531   |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
1532     [apply monotonic_exp1.
1533      apply le_A_exp3.
1534      assumption
1535     |rewrite < times_exp.
1536      rewrite > exp_exp_times.
1537      rewrite > exp_exp_times.
1538      rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1539      rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
1540      apply le_n
1541     ]
1542   ]
1543 qed.
1544