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 (2*n) \le exp (fact n) 2 * A (2*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 (2*n) \le exp 2 (pred (2*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 (2*n) \le exp 2 (pred (2*n)).
1088 intro.cases n
1089   [apply le_n
1090   |cases n1
1091     [simplify.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(2*n) \le (exp 2 (pred (2*n)))*A n.
1299 intro.
1300 apply (trans_le ? (B(2*n)*A n))
1301   [apply le_A_BA
1302   |apply le_times_l.
1303    apply le_B_exp
1304   ]
1305 qed.
1306
1307 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1308 intro.cases n
1309   [apply le_n
1310   |simplify.apply le_plus_r.
1311    apply le_n_Sn
1312   ]
1313 qed.
1314
1315 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1316 intros.
1317 elim H
1318   [apply le_n
1319   |rewrite > times_SSO.
1320    apply le_S_S.
1321    apply (trans_le ? (2*n1))
1322     [assumption
1323     |apply le_n_Sn
1324     ]
1325   ]
1326 qed.
1327
1328 theorem le_A_exp1: \forall n.
1329 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1330 intro.elim n
1331   [simplify.apply le_n
1332   |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1333    apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1334     [apply le_A_exp
1335     |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1336       [apply le_times_r.
1337        assumption
1338       |rewrite < exp_plus_times.
1339        apply le_exp
1340         [apply lt_O_S
1341         |cut (S(S n1) \le 2*(exp 2 n1))
1342           [apply le_S_S_to_le.
1343            change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1344            rewrite < S_pred
1345             [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1346              rewrite < S_pred
1347               [rewrite < eq_minus_plus_plus_minus
1348                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1349                  apply le_n
1350                 |assumption
1351                 ]
1352               |apply lt_to_lt_O_minus.
1353                apply (lt_to_le_to_lt ? (2*(S(S n1))))
1354                 [rewrite > times_n_SO in ⊢ (? % ?).
1355                  rewrite > sym_times.
1356                  apply lt_times_l1
1357                   [apply lt_O_S
1358                   |apply le_n
1359                   ]
1360                 |apply le_times_r.
1361                  assumption
1362                 ]
1363               ]
1364             |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1365              apply le_times
1366               [apply le_n_Sn
1367               |apply lt_O_exp.
1368                apply lt_O_S
1369               ]
1370             ]
1371           |elim n1
1372             [apply le_n
1373             |apply (trans_le ? (2*(S(S n2))))
1374               [apply le_S_times_SSO.
1375                apply lt_O_S
1376               |apply le_times_r.
1377                assumption
1378               ]
1379             ]
1380           ]
1381         ]
1382       ]
1383     ]
1384   ]
1385 qed.
1386
1387 theorem monotonic_A: monotonic nat le A.
1388 unfold.intros.
1389 elim H
1390   [apply le_n
1391   |apply (trans_le ? (A n1))
1392     [assumption
1393     |unfold A.
1394      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1395           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1396       [apply (bool_elim ? (primeb (S n1)));intro
1397         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1398          rewrite > times_n_SO in ⊢ (? % ?).
1399          rewrite > sym_times.
1400          apply le_times
1401           [apply lt_O_exp.apply lt_O_S
1402           |assumption
1403           ]
1404         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1405          assumption
1406         ]
1407       |apply le_pi_p.intros.
1408        apply le_exp
1409         [apply prime_to_lt_O.
1410          apply primeb_true_to_prime.
1411          assumption
1412         |apply le_log
1413           [apply prime_to_lt_SO.
1414            apply primeb_true_to_prime.
1415            assumption
1416           |apply le_S.apply le_n
1417           ]
1418         ]
1419       ]
1420     ]
1421   ]
1422 qed.
1423
1424 (*
1425 theorem le_A_exp2: \forall n. O < n \to
1426 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1427 intros.
1428 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1429   [apply monotonic_A.
1430    apply lt_to_le.
1431    apply lt_exp_log.
1432    apply le_n
1433   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1434     [apply le_A_exp1
1435     |apply le_exp
1436       [apply lt_O_S
1437       |rewrite > assoc_times.apply le_times_r.
1438        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1439        apply le_times_r.
1440        apply le_exp_log.
1441        assumption
1442       ]
1443     ]
1444   ]
1445 qed.
1446 *)
1447
1448 (* example *)
1449 theorem A_SO: A (S O) = S O.
1450 reflexivity.
1451 qed.
1452
1453 theorem A_SSO: A (S(S O)) = S (S O).
1454 reflexivity.
1455 qed.
1456
1457 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1458 reflexivity.
1459 qed.
1460
1461 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1462 reflexivity.
1463 qed.
1464
1465 (* da spostare *)
1466 theorem or_eq_eq_S: \forall n.\exists m.
1467 n = (S(S O))*m \lor n = S ((S(S O))*m).
1468 intro.elim n
1469   [apply (ex_intro ? ? O).
1470    left.reflexivity
1471   |elim H.elim H1
1472     [apply (ex_intro ? ? a).
1473      right.apply eq_f.assumption
1474     |apply (ex_intro ? ? (S a)).
1475      left.rewrite > H2.
1476      apply sym_eq.
1477      apply times_SSO
1478     ]
1479   ]
1480 qed.
1481
1482 (*
1483 (* a better result *)
1484 theorem le_A_exp3: \forall n. S O < n \to
1485 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1486 intro.
1487 apply (nat_elim1 n).
1488 intros.
1489 elim (or_eq_eq_S m).
1490 elim H2
1491   [elim (le_to_or_lt_eq (S O) a)
1492     [rewrite > H3 in ⊢ (? % ?).
1493      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1494       [apply le_A_exp
1495       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1496          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1497         [apply le_times_r.
1498          apply H
1499           [rewrite > H3.
1500            rewrite > times_n_SO in ⊢ (? % ?).
1501            rewrite > sym_times.
1502            apply lt_times_l1
1503             [apply lt_to_le.assumption
1504             |apply le_n
1505             ]
1506           |assumption
1507           ]
1508         |rewrite > sym_times.
1509          rewrite > assoc_times.
1510          rewrite < exp_plus_times.
1511          apply (trans_le ?
1512           (pred 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 < H3.
1519              simplify.
1520              rewrite < plus_n_O.
1521              apply le_S.apply le_S.
1522              apply le_n
1523             ]
1524           |apply le_times_l.
1525            rewrite > times_exp.
1526            apply monotonic_exp1.
1527            rewrite > H3.
1528            rewrite > sym_times.
1529            cases a
1530             [apply le_n
1531             |simplify.
1532              rewrite < plus_n_Sm.
1533              apply le_S.
1534              apply le_n
1535             ]
1536           ]
1537         ]
1538       ]
1539     |rewrite < H4 in H3.
1540      simplify in H3.
1541      rewrite > H3.
1542      simplify.
1543      apply le_S_S.apply le_S_S.apply le_O_n
1544     |apply not_lt_to_le.intro.
1545      apply (lt_to_not_le ? ? H1).
1546      rewrite > H3.
1547      apply (le_n_O_elim a)
1548       [apply le_S_S_to_le.assumption
1549       |apply le_O_n
1550       ]
1551     ]
1552   |elim (le_to_or_lt_eq O a (le_O_n ?))
1553     [apply (trans_le ? (A ((S(S O))*(S a))))
1554       [apply monotonic_A.
1555        rewrite > H3.
1556        rewrite > times_SSO.
1557        apply le_n_Sn
1558       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1559         [apply le_A_exp
1560         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1561            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1562           [apply le_times_r.
1563            apply H
1564             [rewrite > H3.
1565              apply le_S_S.
1566              simplify.
1567              rewrite > plus_n_SO.
1568              apply le_plus_r.
1569              rewrite < plus_n_O.
1570              assumption
1571             |apply le_S_S.assumption
1572             ]
1573           |rewrite > sym_times.
1574            rewrite > assoc_times.
1575            rewrite < exp_plus_times.
1576            apply (trans_le ?
1577             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1578             [rewrite > assoc_times.
1579              apply le_times_r.
1580              rewrite < exp_plus_times.
1581              apply le_exp
1582               [apply lt_O_S
1583               |rewrite > times_SSO.
1584                rewrite < H3.
1585                simplify.
1586                rewrite < plus_n_Sm.
1587                rewrite < plus_n_O.
1588                apply le_n
1589               ]
1590             |apply le_times_l.
1591              rewrite > times_exp.
1592              apply monotonic_exp1.
1593              rewrite > H3.
1594              rewrite > sym_times.
1595              apply le_n
1596             ]
1597           ]
1598         ]
1599       ]
1600     |rewrite < H4 in H3.simplify in H3.
1601      apply False_ind.
1602      apply (lt_to_not_le ? ? H1).
1603      rewrite > H3.
1604      apply le_
1605     ]
1606   ]
1607 qed.
1608 *)
1609
1610 theorem le_A_exp4: \forall n. S O < n \to
1611 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1612 intro.
1613 apply (nat_elim1 n).
1614 intros.
1615 elim (or_eq_eq_S m).
1616 elim H2
1617   [elim (le_to_or_lt_eq (S O) a)
1618     [rewrite > H3 in ⊢ (? % ?).
1619      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1620       [apply le_A_exp
1621       |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1622         [apply le_times_r.
1623          apply H
1624           [rewrite > H3.
1625            rewrite > times_n_SO in ⊢ (? % ?).
1626            rewrite > sym_times.
1627            apply lt_times_l1
1628             [apply lt_to_le.assumption
1629             |apply le_n
1630             ]
1631           |assumption
1632           ]
1633         |rewrite < H3.
1634          rewrite < assoc_times.
1635          rewrite > sym_times in ⊢ (? (? % ?) ?).
1636          rewrite > assoc_times.
1637          apply le_times
1638           [rewrite > H3.
1639            elim a[apply le_n|simplify.apply le_plus_n_r]
1640           |rewrite < exp_plus_times.
1641            apply le_exp
1642             [apply lt_O_S
1643             |apply (trans_le ? (m+(m-3)))
1644               [apply le_plus_l.
1645                cases m[apply le_n|apply le_n_Sn]
1646               |simplify.rewrite < plus_n_O.
1647                rewrite > eq_minus_plus_plus_minus
1648                 [apply le_n
1649                 |rewrite > H3.
1650                  apply (trans_le ? (2*2))
1651                   [simplify.apply (le_n_Sn 3)
1652                   |apply le_times_r.assumption
1653                   ]
1654                 ]
1655               ]
1656             ]
1657           ]
1658         ]
1659       ]
1660     |rewrite > H3.rewrite < H4.simplify.
1661      apply le_S_S.apply lt_O_S
1662     |apply not_lt_to_le.intro.
1663      apply (lt_to_not_le ? ? H1).
1664      rewrite > H3.
1665      apply (le_n_O_elim a)
1666       [apply le_S_S_to_le.assumption
1667       |apply le_O_n
1668       ]
1669     ]
1670   |elim (le_to_or_lt_eq O a (le_O_n ?))
1671     [apply (trans_le ? (A ((S(S O))*(S a))))
1672       [apply monotonic_A.
1673        rewrite > H3.
1674        rewrite > times_SSO.
1675        apply le_n_Sn
1676       |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1677         [apply le_A_exp
1678         |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1679           [apply le_times_r.
1680            apply H
1681             [rewrite > H3.
1682              apply le_S_S.
1683              apply le_S_times_SSO.
1684              assumption
1685             |apply le_S_S.assumption
1686             ]
1687           |rewrite > H3.
1688            change in ⊢ (? ? (? % ?)) with (2*a).
1689            rewrite > times_SSO.
1690            change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1691            rewrite > minus_Sn_m
1692             [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1693              rewrite < assoc_times in ⊢ (? (? ? %) ?).
1694              rewrite < assoc_times.
1695              rewrite > sym_times in ⊢ (? (? % ?) ?).
1696              rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1697              rewrite > assoc_times.
1698              apply le_times_r.
1699              rewrite < exp_plus_times.
1700              apply le_exp
1701               [apply lt_O_S
1702               |rewrite < eq_minus_plus_plus_minus
1703                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1704                  apply le_n
1705                 |apply le_S_S.
1706                  apply O_lt_const_to_le_times_const.
1707                  assumption
1708                 ]
1709               ]
1710             |apply le_S_S.
1711              apply O_lt_const_to_le_times_const.
1712              assumption
1713             ]
1714           ]
1715         ]
1716       ]
1717     |rewrite < H4 in H3.simplify in H3.
1718      apply False_ind.
1719      apply (lt_to_not_le ? ? H1).
1720      rewrite > H3.
1721      apply le_n
1722     ]
1723   ]
1724 qed.
1725
1726 theorem eq_sigma_pi_SO_n: \forall n.
1727 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1728 intro.elim n
1729   [reflexivity
1730   |rewrite > true_to_sigma_p_Sn
1731     [rewrite > H.reflexivity
1732     |reflexivity
1733     ]
1734   ]
1735 qed.
1736
1737 theorem leA_prim: \forall n.
1738 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1739 intro.
1740 unfold prim.
1741 rewrite < (exp_sigma_p (S n) n primeb).
1742 unfold A.
1743 rewrite < times_pi_p.
1744 apply le_pi_p.
1745 intros.
1746 rewrite > sym_times.
1747 change in ⊢ (? ? %) with (exp i (S (log i n))).
1748 apply lt_to_le.
1749 apply lt_exp_log.
1750 apply prime_to_lt_SO.
1751 apply primeb_true_to_prime.
1752 assumption.
1753 qed.
1754
1755
1756 theorem le_prim_log : \forall n,b.S O < b \to
1757 log b (A n) \leq prim n * (S (log b n)).
1758 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
1759   [apply le_log
1760      [assumption
1761      |apply le_Al]
1762   |assumption]
1763 qed.
1764
1765
1766 (* the inequalities *)
1767 theorem le_exp_priml: \forall n. O < n \to
1768 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1769 intros.
1770 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1771   [apply le_exp_B.assumption
1772   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1773    apply le_times_r.
1774    apply (trans_le ? (A ((S(S O))*n)))
1775     [apply le_B_A
1776     |apply le_Al
1777     ]
1778   ]
1779 qed.
1780
1781 alias num (instance 0) = "natural number".
1782
1783 theorem le_exp_prim4l: \forall n. O < n \to
1784 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
1785 intros.
1786 apply (trans_le ? (2*(4*n*(B (4*n)))))
1787   [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
1788    apply le_times_r.
1789    cut (4*n = 2*(2*n))
1790     [rewrite > Hcut.
1791      apply le_exp_B.
1792      apply lt_to_le.unfold.
1793      rewrite > times_n_SO in ⊢ (? % ?).
1794      apply le_times_r.assumption
1795     |rewrite < assoc_times.
1796      reflexivity
1797     ]
1798   |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
1799    rewrite < assoc_times.
1800    rewrite > sym_times in ⊢ (? (? % ?) ?).
1801    rewrite > assoc_times.
1802    apply le_times_r.
1803    apply (trans_le ? (A (4*n)))
1804     [apply le_B_A4.assumption
1805     |apply le_Al
1806     ]
1807   ]
1808 qed.
1809
1810 theorem le_priml: \forall n. O < n \to
1811 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1812 intros.
1813 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1814   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1815     [apply le_log
1816       [apply le_n
1817       |apply le_exp_priml.assumption
1818       ]
1819     |rewrite > sym_times in ⊢ (? ? %).
1820      apply log_exp1.
1821      apply le_n
1822     ]
1823   |apply le_n
1824   ]
1825 qed.
1826
1827 theorem le_exp_primr: \forall n. S O < n \to
1828 exp n (prim n) \le exp (pred n) 2*(exp 2 (2*(2*n-3))).
1829 intros.
1830 apply (trans_le ? (exp (A n) 2))
1831   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1832    rewrite < times_n_SO.
1833    apply leA_r2
1834   |apply (trans_le ? (exp ((pred n)*(exp 2 (2*n - 3))) 2))
1835     [apply monotonic_exp1.
1836      apply le_A_exp4.
1837      assumption
1838     |rewrite < times_exp.
1839      rewrite > exp_exp_times.
1840      apply le_times_r.
1841      rewrite > sym_times.
1842      apply le_n
1843     ]
1844   ]
1845 qed.
1846