helm/software/matita/library/nat/chebyshev.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/chebishev".
  16
  17 include "nat/log.ma".
  18 include "nat/pi_p.ma".
  19 include "nat/factorization.ma".
  20 include "nat/factorial2.ma".
  21
  22 definition prim: nat \to nat \def
  23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
  24
  25 (* This is chebishev psi function *)
  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_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n).
 979 intros.unfold B.
 980 rewrite > eq_A_A'.
 981 unfold A'.
 982 cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
 983   [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
 984     [rewrite > (pi_p_gi ? ? (S(S O)))
 985       [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
 986         [rewrite < assoc_times.
 987          apply le_times
 988           [rewrite > (pi_p_gi ? ? O)
 989             [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
 990               [rewrite < assoc_times.
 991                apply le_times
 992                 [rewrite < exp_n_SO.
 993                  change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
 994                  with ((S(S O))*(S(S O))).
 995                  rewrite > assoc_times.
 996                  rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
 997                  rewrite > lt_O_to_div_times
 998                   [rewrite > divides_to_mod_O
 999                     [apply le_n
1000                     |apply lt_O_S
1001                     |apply (witness ? ? n).reflexivity
1002                     ]
1003                   |apply lt_O_S
1004                   ]
1005                 |apply le_pi_p.intros.
1006                  rewrite > exp_n_SO in ⊢ (? ? %).
1007                  apply le_exp
1008                   [apply lt_O_S
1009                   |apply le_S_S_to_le.
1010                    apply lt_mod_m_m.
1011                    apply lt_O_S
1012                   ]
1013                 ]
1014               |assumption
1015               |reflexivity
1016               ]
1017             |assumption
1018             |reflexivity
1019             ]
1020           |apply le_pi_p.intros.
1021            apply le_pi_p.intros.
1022            rewrite > exp_n_SO in ⊢ (? ? %).
1023            apply le_exp
1024             [apply prime_to_lt_O.
1025              apply primeb_true_to_prime.
1026              apply (andb_true_true ? ? H2)
1027             |apply le_S_S_to_le.
1028              apply lt_mod_m_m.
1029              apply lt_O_S
1030             ]
1031           ]
1032         |assumption
1033         |reflexivity
1034         ]
1035       |assumption
1036       |reflexivity
1037       ]
1038     |apply lt_O_log
1039       [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
1040        apply lt_times_r1
1041         [apply lt_O_S
1042         |assumption
1043         ]
1044       |rewrite > times_n_SO in ⊢ (? % ?).
1045        apply le_times
1046         [apply le_S.apply le_S.apply le_n
1047         |assumption
1048         ]
1049       ]
1050     ]
1051   |apply le_S_S.
1052    rewrite > times_n_SO in ⊢ (? % ?).
1053    apply le_times
1054     [apply le_S.apply le_n_Sn
1055     |assumption
1056     ]
1057   ]
1058 qed.
1059
1060 theorem le_fact_A:\forall n.S O < n \to
1061 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
1062 intros.
1063 rewrite > eq_fact_B
1064   [apply le_times_r.
1065    apply le_B_A
1066   |assumption
1067   ]
1068 qed.
1069
1070 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1071 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1072 intros.
1073 apply (le_times_to_le (exp (fact n) (S(S O))))
1074   [apply lt_O_exp.
1075    apply lt_O_fact
1076   |rewrite < eq_fact_B
1077     [rewrite < sym_times in ⊢ (? ? %).
1078      rewrite > exp_SSO.
1079      rewrite < assoc_times.
1080      apply fact1
1081     |assumption
1082     ]
1083   ]
1084 qed.
1085
1086 theorem le_B_exp: \forall n.
1087 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1088 intro.cases n
1089   [apply le_n
1090   |cases n1
1091     [simplify.apply le_S.apply le_S.apply le_n
1092     |apply lt_SO_to_le_B_exp.
1093      apply le_S_S.apply lt_O_S.
1094     ]
1095   ]
1096 qed.
1097
1098 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1099 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1100 intros.
1101 apply (le_times_to_le (exp (fact n) (S(S O))))
1102   [apply lt_O_exp.
1103    apply lt_O_fact
1104   |rewrite < assoc_times in ⊢ (? ? %).
1105    rewrite > sym_times in ⊢ (? ? (? % ?)).
1106    rewrite > assoc_times in ⊢ (? ? %).
1107    rewrite < eq_fact_B
1108     [rewrite < sym_times.
1109      apply fact3.
1110      apply lt_to_le.assumption
1111     |assumption
1112     ]
1113   ]
1114 qed.
1115
1116 theorem le_exp_B: \forall n. O < n \to
1117 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1118 intros.
1119 elim H
1120   [apply le_n
1121   |apply lt_SO_to_le_exp_B.
1122    apply le_S_S.assumption
1123   ]
1124 qed.
1125
1126 theorem eq_A_SSO_n: \forall n.O < n \to
1127 A((S(S O))*n) =
1128  pi_p (S ((S(S O))*n)) primeb
1129   (\lambda p.(pi_p (log p ((S(S O))*n) )
1130     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1131  *A n.
1132 intro.
1133 rewrite > eq_A_A'.rewrite > eq_A_A'.
1134 unfold A'.intros.
1135 cut (
1136  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1137  = pi_p (S ((S(S O))*n)) primeb
1138     (λ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))))))))
1139   [rewrite > Hcut.
1140    rewrite < times_pi_p.
1141    apply eq_pi_p1;intros
1142     [reflexivity
1143     |rewrite < times_pi_p.
1144      apply eq_pi_p;intros
1145       [reflexivity
1146       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1147         [simplify.rewrite < times_n_SO.apply times_n_SO
1148         |simplify.rewrite < plus_n_O.apply times_n_SO
1149         ]
1150       ]
1151     ]
1152   |apply (trans_eq ? ? (pi_p (S n) primeb
1153     (\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))))))))
1154     [apply eq_pi_p1;intros
1155       [reflexivity
1156       |apply eq_pi_p1;intros
1157         [reflexivity
1158         |rewrite > lt_to_leb_false
1159           [simplify.apply times_n_SO
1160           |apply le_S_S.
1161            apply (trans_le ? (exp x (log x 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              assumption
1170             ]
1171           ]
1172         ]
1173       ]
1174     |apply (trans_eq ? ?
1175       (pi_p (S ((S(S O))*n)) primeb
1176        (λp:nat.pi_p (log p n) (λi:nat.true)
1177         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1178       [apply sym_eq.
1179        apply or_false_eq_SO_to_eq_pi_p
1180         [apply le_S_S.
1181          simplify.
1182          apply le_plus_n_r
1183         |intros.right.
1184          rewrite > lt_to_log_O
1185           [reflexivity
1186           |assumption
1187           |assumption
1188           ]
1189         ]
1190       |apply eq_pi_p1;intros
1191         [reflexivity
1192         |apply sym_eq.
1193          apply or_false_eq_SO_to_eq_pi_p
1194           [apply le_log
1195             [apply prime_to_lt_SO.
1196              apply primeb_true_to_prime.
1197              assumption
1198             |simplify.
1199              apply le_plus_n_r
1200             ]
1201           |intros.right.
1202            rewrite > le_to_leb_true
1203             [simplify.reflexivity
1204             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1205               [apply lt_exp_log.
1206                apply prime_to_lt_SO.
1207                apply primeb_true_to_prime.
1208                assumption
1209               |apply le_exp
1210                 [apply prime_to_lt_O.
1211                  apply primeb_true_to_prime.
1212                  assumption
1213                 |apply le_S_S.assumption
1214                 ]
1215               ]
1216             ]
1217           ]
1218         ]
1219       ]
1220     ]
1221   ]
1222 qed.
1223
1224 theorem le_A_BA1: \forall n. O < n \to
1225 A((S(S O))*n) \le B((S(S O))*n)*A n.
1226 intros.
1227 rewrite > eq_A_SSO_n
1228   [apply le_times_l.
1229    unfold B.
1230    apply le_pi_p.intros.
1231    apply le_pi_p.intros.
1232    apply le_exp
1233     [apply prime_to_lt_O.
1234      apply primeb_true_to_prime.
1235      assumption
1236     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1237       [simplify in ⊢ (? % ?).
1238        cut ((S(S O))*n/i\sup(S i1) = S O)
1239         [rewrite > Hcut.apply le_n
1240         |apply (div_mod_spec_to_eq
1241           ((S(S O))*n) (exp i (S i1))
1242            ? (mod ((S(S O))*n) (exp i (S i1)))
1243            ? (minus ((S(S O))*n) (exp i (S i1))) )
1244           [apply div_mod_spec_div_mod.
1245            apply lt_O_exp.
1246            apply prime_to_lt_O.
1247            apply primeb_true_to_prime.
1248            assumption
1249           |cut (i\sup(S i1)≤(S(S O))*n)
1250             [apply div_mod_spec_intro
1251               [apply lt_plus_to_lt_minus
1252                 [assumption
1253                 |simplify in ⊢ (? % ?).
1254                  rewrite < plus_n_O.
1255                  apply lt_plus
1256                   [apply leb_true_to_le.assumption
1257                   |apply leb_true_to_le.assumption
1258                   ]
1259                 ]
1260               |rewrite > sym_plus.
1261                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1262                rewrite < times_n_SO.
1263                apply plus_minus_m_m.
1264                assumption
1265               ]
1266             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1267               [apply le_exp
1268                 [apply prime_to_lt_O.
1269                  apply primeb_true_to_prime.
1270                  assumption
1271                 |assumption
1272                 ]
1273               |apply le_exp_log.
1274                rewrite > (times_n_O O) in ⊢ (? % ?).
1275                apply lt_times
1276                 [apply lt_O_S
1277                 |assumption
1278                 ]
1279               ]
1280             ]
1281           ]
1282         ]
1283       |apply le_O_n
1284       ]
1285     ]
1286   |assumption
1287   ]
1288 qed.
1289
1290 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1291 intros.cases n
1292   [apply le_n
1293   |apply le_A_BA1.apply lt_O_S
1294   ]
1295 qed.
1296
1297 theorem le_A_exp: \forall n.
1298 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1299 intro.
1300 apply (trans_le ? (B((S(S O))*n)*A n))
1301   [apply le_A_BA
1302   |apply le_times_l.
1303    apply le_B_exp
1304   ]
1305 qed.
1306
1307 theorem le_A_exp1: \forall n.
1308 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1309 intro.elim n
1310   [simplify.apply le_S_S.apply le_O_n
1311   |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1312    apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1313     [apply le_A_exp
1314     |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))))
1315       [apply le_times_r.
1316        assumption
1317       |rewrite < exp_plus_times.
1318        simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1319        apply le_n
1320       ]
1321     ]
1322   ]
1323 qed.
1324
1325 theorem monotonic_A: monotonic nat le A.
1326 unfold.intros.
1327 elim H
1328   [apply le_n
1329   |apply (trans_le ? (A n1))
1330     [assumption
1331     |unfold A.
1332      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1333           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1334       [apply (bool_elim ? (primeb (S n1)));intro
1335         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1336          rewrite > times_n_SO in ⊢ (? % ?).
1337          rewrite > sym_times.
1338          apply le_times
1339           [apply lt_O_exp.apply lt_O_S
1340           |assumption
1341           ]
1342         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1343          assumption
1344         ]
1345       |apply le_pi_p.intros.
1346        apply le_exp
1347         [apply prime_to_lt_O.
1348          apply primeb_true_to_prime.
1349          assumption
1350         |apply le_log
1351           [apply prime_to_lt_SO.
1352            apply primeb_true_to_prime.
1353            assumption
1354           |apply le_S.apply le_n
1355           ]
1356         ]
1357       ]
1358     ]
1359   ]
1360 qed.
1361
1362 theorem le_A_exp2: \forall n. O < n \to
1363 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1364 intros.
1365 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1366   [apply monotonic_A.
1367    apply lt_to_le.
1368    apply lt_exp_log.
1369    apply le_n
1370   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1371     [apply le_A_exp1
1372     |apply le_exp
1373       [apply lt_O_S
1374       |rewrite > assoc_times.apply le_times_r.
1375        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1376        apply le_times_r.
1377        apply le_exp_log.
1378        assumption
1379       ]
1380     ]
1381   ]
1382 qed.
1383
1384 (* example *)
1385 theorem A_SO: A (S O) = S O.
1386 reflexivity.
1387 qed.
1388
1389 theorem A_SSO: A (S(S O)) = S (S O).
1390 reflexivity.
1391 qed.
1392
1393 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1394 reflexivity.
1395 qed.
1396
1397 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1398 reflexivity.
1399 qed.
1400
1401 (* da spostare *)
1402 theorem or_eq_eq_S: \forall n.\exists m.
1403 n = (S(S O))*m \lor n = S ((S(S O))*m).
1404 intro.elim n
1405   [apply (ex_intro ? ? O).
1406    left.reflexivity
1407   |elim H.elim H1
1408     [apply (ex_intro ? ? a).
1409      right.apply eq_f.assumption
1410     |apply (ex_intro ? ? (S a)).
1411      left.rewrite > H2.
1412      apply sym_eq.
1413      apply times_SSO
1414     ]
1415   ]
1416 qed.
1417
1418 (* a better result *)
1419 theorem le_A_exp3: \forall n. S O < n \to
1420 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1421 intro.
1422 apply (nat_elim1 n).
1423 intros.
1424 elim (or_eq_eq_S m).
1425 elim H2
1426   [elim (le_to_or_lt_eq (S O) a)
1427     [rewrite > H3 in ⊢ (? % ?).
1428      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1429       [apply le_A_exp
1430       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1431          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1432         [apply le_times_r.
1433          apply H
1434           [rewrite > H3.
1435            rewrite > times_n_SO in ⊢ (? % ?).
1436            rewrite > sym_times.
1437            apply lt_times_l1
1438             [apply lt_to_le.assumption
1439             |apply le_n
1440             ]
1441           |assumption
1442           ]
1443         |rewrite > sym_times.
1444          rewrite > assoc_times.
1445          rewrite < exp_plus_times.
1446          apply (trans_le ?
1447           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1448           [rewrite > assoc_times.
1449            apply le_times_r.
1450            rewrite < exp_plus_times.
1451            apply le_exp
1452             [apply lt_O_S
1453             |rewrite < H3.
1454              simplify.
1455              rewrite < plus_n_O.
1456              apply le_S.apply le_S.
1457              apply le_n
1458             ]
1459           |apply le_times_l.
1460            rewrite > times_exp.
1461            apply monotonic_exp1.
1462            rewrite > H3.
1463            rewrite > sym_times.
1464            cases a
1465             [apply le_n
1466             |simplify.
1467              rewrite < plus_n_Sm.
1468              apply le_S.
1469              apply le_n
1470             ]
1471           ]
1472         ]
1473       ]
1474     |rewrite < H4 in H3.
1475      simplify in H3.
1476      rewrite > H3.
1477      simplify.
1478      apply le_S_S.apply le_S_S.apply le_O_n
1479     |apply not_lt_to_le.intro.
1480      apply (lt_to_not_le ? ? H1).
1481      rewrite > H3.
1482      apply (le_n_O_elim a)
1483       [apply le_S_S_to_le.assumption
1484       |apply le_O_n
1485       ]
1486     ]
1487   |elim (le_to_or_lt_eq O a (le_O_n ?))
1488     [apply (trans_le ? (A ((S(S O))*(S a))))
1489       [apply monotonic_A.
1490        rewrite > H3.
1491        rewrite > times_SSO.
1492        apply le_n_Sn
1493       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1494         [apply le_A_exp
1495         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1496            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1497           [apply le_times_r.
1498            apply H
1499             [rewrite > H3.
1500              apply le_S_S.
1501              simplify.
1502              rewrite > plus_n_SO.
1503              apply le_plus_r.
1504              rewrite < plus_n_O.
1505              assumption
1506             |apply le_S_S.assumption
1507             ]
1508           |rewrite > sym_times.
1509            rewrite > assoc_times.
1510            rewrite < exp_plus_times.
1511            apply (trans_le ?
1512             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1513             [rewrite > assoc_times.
1514              apply le_times_r.
1515              rewrite < exp_plus_times.
1516              apply le_exp
1517               [apply lt_O_S
1518               |rewrite > times_SSO.
1519                rewrite < H3.
1520                simplify.
1521                rewrite < plus_n_Sm.
1522                rewrite < plus_n_O.
1523                apply le_n
1524               ]
1525             |apply le_times_l.
1526              rewrite > times_exp.
1527              apply monotonic_exp1.
1528              rewrite > H3.
1529              rewrite > sym_times.
1530              apply le_n
1531             ]
1532           ]
1533         ]
1534       ]
1535     |rewrite < H4 in H3.simplify in H3.
1536      apply False_ind.
1537      apply (lt_to_not_le ? ? H1).
1538      rewrite > H3.
1539      apply le_n
1540     ]
1541   ]
1542 qed.
1543
1544 theorem le_A_exp4: \forall n. S O < n \to
1545 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))).
1546 intro.
1547 apply (nat_elim1 n).
1548 intros.
1549 elim (or_eq_eq_S m).
1550 elim H2
1551   [elim (le_to_or_lt_eq (S O) a)
1552     [rewrite > H3 in ⊢ (? % ?).
1553      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1554       [apply le_A_exp
1555       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1556          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*(pred a)))))
1557         [apply le_times_r.
1558          apply H
1559           [rewrite > H3.
1560            rewrite > times_n_SO in ⊢ (? % ?).
1561            rewrite > sym_times.
1562            apply lt_times_l1
1563             [apply lt_to_le.assumption
1564             |apply le_n
1565             ]
1566           |assumption
1567           ]
1568         |rewrite > sym_times.
1569          rewrite > assoc_times.
1570          rewrite < exp_plus_times.
1571          apply (trans_le ?
1572           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*(pred m))))
1573           [rewrite > assoc_times.
1574            apply le_times_r.
1575            rewrite < exp_plus_times.
1576            apply le_exp
1577             [apply lt_O_S
1578             |rewrite < H3.
1579              simplify.
1580              rewrite < plus_n_O.
1581              apply le_S.apply le_S.
1582              rewrite < plus_n_O;
1583              apply le_S_S_to_le;
1584              rewrite > plus_n_Sm in \vdash (? ? %);
1585              rewrite < S_pred;
1586                [change in \vdash (? % ?) with ((S (pred a + pred a)) + m);
1587                 apply le_plus_l;
1588                 apply le_S_S_to_le;
1589                 rewrite < S_pred;
1590                   [rewrite > plus_n_Sm;rewrite > sym_plus;
1591                    rewrite > plus_n_Sm;
1592                    rewrite > H3;simplify in \vdash (? ? %);
1593                    rewrite < plus_n_O;rewrite < S_pred;
1594                      [apply le_n
1595                      |apply lt_to_le;assumption]
1596                   |apply lt_to_le;assumption]
1597                |apply lt_to_le;assumption]]
1598           |apply le_times_l.
1599            rewrite > times_exp.
1600            apply monotonic_exp1.
1601            rewrite > H3.
1602            rewrite > sym_times.
1603            cases a
1604             [apply le_n
1605             |simplify.
1606              rewrite < plus_n_Sm.
1607              apply le_S.
1608              apply le_n
1609             ]
1610           ]
1611         ]
1612       ]
1613     |rewrite < H4 in H3.
1614      simplify in H3.
1615      rewrite > H3.
1616      simplify.
1617      apply le_S_S.apply le_S_S.apply le_O_n
1618     |apply not_lt_to_le.intro.
1619      apply (lt_to_not_le ? ? H1).
1620      rewrite > H3.
1621      apply (le_n_O_elim a)
1622       [apply le_S_S_to_le.assumption
1623       |apply le_O_n
1624       ]
1625     ]
1626   |elim (le_to_or_lt_eq O a (le_O_n ?))
1627     [apply (trans_le ? (A ((S(S O))*(S a))))
1628       [apply monotonic_A.
1629        rewrite > H3.
1630        rewrite > times_SSO.
1631        apply le_n_Sn
1632       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1633         [apply le_A_exp
1634         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1635            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1636           [apply le_times_r.
1637            apply (trans_le ? ? ? (H (S a) ? ?));
1638             [rewrite > H3.
1639              apply le_S_S.
1640              simplify.
1641              rewrite > plus_n_SO.
1642              apply le_plus_r.
1643              rewrite < plus_n_O.
1644              assumption
1645             |apply le_S_S.assumption
1646             |simplify in ⊢ (? (? (? % ?) ?) ?);
1647              apply le_times_r;apply le_exp;
1648                [apply le_S;apply le_n
1649                |apply le_times_r;simplify;apply le_n]
1650             ]
1651           |rewrite > sym_times.
1652            rewrite > assoc_times.
1653            rewrite < exp_plus_times.
1654            rewrite > H3;
1655            change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a);
1656            rewrite < times_exp;
1657            rewrite < sym_times in \vdash (? ? (? % ?));
1658            rewrite > assoc_times;
1659            apply le_times_r;
1660            rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?);
1661            rewrite > sym_plus in \vdash (? (? ? %) ?);
1662            rewrite > assoc_plus in \vdash (? (? ? %) ?);
1663            rewrite > exp_plus_times;apply le_times_r;
1664            rewrite < distr_times_plus in ⊢ (? (? ? %) ?);
1665            simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O;
1666            apply le_n
1667           ]
1668         ]
1669       ]
1670     |rewrite < H4 in H3.simplify in H3.
1671      apply False_ind.
1672      apply (lt_to_not_le ? ? H1).
1673      rewrite > H3.
1674      apply le_n
1675     ]
1676   ]
1677 qed.
1678
1679 theorem eq_sigma_pi_SO_n: \forall n.
1680 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1681 intro.elim n
1682   [reflexivity
1683   |rewrite > true_to_sigma_p_Sn
1684     [rewrite > H.reflexivity
1685     |reflexivity
1686     ]
1687   ]
1688 qed.
1689
1690 theorem leA_prim: \forall n.
1691 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1692 intro.
1693 unfold prim.
1694 rewrite < (exp_sigma_p (S n) n primeb).
1695 unfold A.
1696 rewrite < times_pi_p.
1697 apply le_pi_p.
1698 intros.
1699 rewrite > sym_times.
1700 change in ⊢ (? ? %) with (exp i (S (log i n))).
1701 apply lt_to_le.
1702 apply lt_exp_log.
1703 apply prime_to_lt_SO.
1704 apply primeb_true_to_prime.
1705 assumption.
1706 qed.
1707
1708
1709 theorem le_prim_log : \forall n,b.S O < b \to
1710 log b (A n) \leq prim n * (S (log b n)).
1711 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
1712   [apply le_log
1713      [assumption
1714      |apply le_Al]
1715   |assumption]
1716 qed.
1717
1718
1719 (* the inequalities *)
1720 theorem le_exp_priml: \forall n. O < n \to
1721 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1722 intros.
1723 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1724   [apply le_exp_B.assumption
1725   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1726    apply le_times_r.
1727    apply (trans_le ? (A ((S(S O))*n)))
1728     [apply le_B_A
1729     |apply le_Al
1730     ]
1731   ]
1732 qed.
1733
1734 alias num (instance 0) = "natural number".
1735
1736 theorem le_exp_prim4l: \forall n. O < n \to
1737 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
1738 intros.
1739 apply (trans_le ? (2*(4*n*(B (4*n)))))
1740   [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
1741    apply le_times_r.
1742    cut (4*n = 2*(2*n))
1743     [rewrite > Hcut.
1744      apply le_exp_B.
1745      apply lt_to_le.unfold.
1746      rewrite > times_n_SO in ⊢ (? % ?).
1747      apply le_times_r.assumption
1748     |rewrite < assoc_times.
1749      reflexivity
1750     ]
1751   |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
1752    rewrite < assoc_times.
1753    rewrite > sym_times in ⊢ (? (? % ?) ?).
1754    rewrite > assoc_times.
1755    apply le_times_r.
1756    apply (trans_le ? (A (4*n)))
1757     [apply le_B_A4.assumption
1758     |apply le_Al
1759     ]
1760   ]
1761 qed.
1762
1763 theorem le_priml: \forall n. O < n \to
1764 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1765 intros.
1766 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1767   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1768     [apply le_log
1769       [apply le_n
1770       |apply le_exp_priml.assumption
1771       ]
1772     |rewrite > sym_times in ⊢ (? ? %).
1773      apply log_exp1.
1774      apply le_n
1775     ]
1776   |apply le_n
1777   ]
1778 qed.
1779
1780 theorem le_exp_primr: \forall n. S O < n \to
1781 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * (pred n))).
1782 intros.
1783 apply (trans_le ? (exp (A n) (S(S O))))
1784   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1785    rewrite < times_n_SO.
1786    apply leA_r2
1787   |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n)))) (S(S O))))
1788     [apply monotonic_exp1.
1789      apply le_A_exp4.
1790      assumption
1791     |rewrite < times_exp.
1792      rewrite > exp_exp_times.
1793      rewrite > exp_exp_times.
1794      rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1795      rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
1796      apply le_n
1797     ]
1798   ]
1799 qed.
1800