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 include "nat/log.ma".
  16 include "nat/pi_p.ma".
  17 include "nat/factorization.ma".
  18 include "nat/factorial2.ma".
  19
  20 definition prim: nat \to nat \def
  21 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
  22
  23 (* This is chebishev psi function *)
  24 definition A: nat \to nat \def
  25 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
  26
  27 theorem le_Al1: \forall n.
  28 A n \le pi_p (S n) primeb (\lambda p.n).
  29 intro.unfold A.
  30 cases n
  31   [simplify.apply le_n
  32   |apply le_pi_p.
  33    intros.
  34    apply le_exp_log.
  35    apply lt_O_S
  36   ]
  37 qed.
  38
  39 theorem le_Al: \forall n.
  40 A n \le exp n (prim n).
  41 intro.unfold prim.
  42 rewrite < exp_sigma_p.
  43 apply le_Al1.
  44 qed.
  45
  46 theorem leA_r2: \forall n.
  47 exp n (prim n) \le A n * A n.
  48 intro.unfold prim.
  49 elim (le_to_or_lt_eq ? ? (le_O_n n))
  50   [rewrite < (exp_sigma_p (S n) n primeb).
  51    unfold A.
  52    rewrite < times_pi_p.
  53    apply le_pi_p.
  54    intros.
  55    rewrite < exp_plus_times.
  56    apply (trans_le ? (exp i (S(log i n))))
  57     [apply lt_to_le.
  58      apply lt_exp_log.
  59      apply prime_to_lt_SO.
  60      apply primeb_true_to_prime.
  61      assumption
  62     |apply le_exp
  63       [apply prime_to_lt_O.
  64        apply primeb_true_to_prime.
  65        assumption
  66       |rewrite > plus_n_O.
  67        simplify.
  68        rewrite > plus_n_Sm.
  69        apply le_plus_r.
  70        apply lt_O_log
  71         [assumption
  72         |apply le_S_S_to_le.
  73          apply H1
  74         ]
  75       ]
  76     ]
  77   |rewrite < H. apply le_n
  78   ]
  79 qed.
  80
  81 (* an equivalent formulation for psi *)
  82 definition A': nat \to nat \def
  83 \lambda n. pi_p (S n) primeb
  84   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
  85
  86 theorem eq_A_A': \forall n.A n = A' n.
  87 intro.unfold A.unfold A'.
  88 apply eq_pi_p
  89   [intros.reflexivity
  90   |intros.
  91    apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
  92     [apply eq_f.apply sym_eq.apply sigma_p_true
  93     |apply sym_eq.apply exp_sigma_p
  94     ]
  95   ]
  96 qed.
  97
  98 theorem eq_pi_p_primeb_divides_b: \forall n,m.
  99 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
 100 = pi_p n primeb (\lambda p.exp p (ord m p)).
 101 intro.
 102 elim n
 103   [reflexivity
 104   |apply (bool_elim ? (primeb n1));intro
 105     [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
 106       [apply (bool_elim ? (divides_b n1 m));intro
 107         [rewrite > true_to_pi_p_Sn
 108           [apply eq_f.
 109            apply H
 110           |apply true_to_true_to_andb_true;assumption
 111           ]
 112         |rewrite > false_to_pi_p_Sn
 113           [rewrite > not_divides_to_ord_O
 114             [simplify in ⊢ (? ? ? (? % ?)).
 115              rewrite > sym_times.
 116              rewrite < times_n_SO.
 117              apply H
 118             |apply primeb_true_to_prime.assumption
 119             |apply divides_b_false_to_not_divides.
 120              assumption
 121             ]
 122           |rewrite > H1.rewrite > H2.reflexivity
 123           ]
 124         ]
 125       |assumption
 126       ]
 127     |rewrite > false_to_pi_p_Sn
 128       [rewrite > false_to_pi_p_Sn
 129         [apply H
 130         |assumption
 131         ]
 132       |rewrite > H1.reflexivity
 133       ]
 134     ]
 135   ]
 136 qed.
 137
 138 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
 139 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
 140 intro.elim q
 141   [apply False_ind.
 142    apply (not_le_Sn_O ? H1)
 143   |apply (bool_elim ? (primeb n∧divides_b n m));intro
 144     [rewrite > true_to_pi_p_Sn
 145       [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
 146         [apply eq_f.
 147          rewrite > (H (ord_rem m n))
 148           [apply eq_pi_p1
 149             [intros.
 150              apply (bool_elim ? (primeb x));intro
 151               [simplify.
 152                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
 153                 [apply sym_eq.
 154                  apply divides_to_divides_b_true
 155                   [apply prime_to_lt_O.
 156                    apply primeb_true_to_prime.
 157                    assumption
 158                   |apply (trans_divides ? (ord_rem m n))
 159                     [apply divides_b_true_to_divides.
 160                      assumption
 161                     |apply divides_ord_rem
 162                       [apply (trans_lt ? x)
 163                         [apply prime_to_lt_SO.
 164                          apply primeb_true_to_prime.
 165                          assumption
 166                         |assumption
 167                         ]
 168                       |assumption
 169                       ]
 170                     ]
 171                   ]
 172                 |apply sym_eq.
 173                  apply not_divides_to_divides_b_false
 174                   [apply prime_to_lt_O.
 175                    apply primeb_true_to_prime.
 176                    assumption
 177                   |apply ord_O_to_not_divides
 178                     [assumption
 179                     |apply primeb_true_to_prime.
 180                      assumption
 181                     |rewrite < (ord_ord_rem n)
 182                       [apply not_divides_to_ord_O
 183                         [apply primeb_true_to_prime.
 184                          assumption
 185                         |apply divides_b_false_to_not_divides.
 186                          assumption
 187                         ]
 188                       |assumption
 189                       |apply primeb_true_to_prime.
 190                        apply (andb_true_true ? ? H3)
 191                       |apply primeb_true_to_prime.
 192                        assumption
 193                       |assumption
 194                       ]
 195                     ]
 196                   ]
 197                 ]
 198               |reflexivity
 199               ]
 200             |intros.
 201              apply eq_f.
 202              apply ord_ord_rem
 203               [assumption
 204               |apply primeb_true_to_prime.
 205                apply (andb_true_true ? ? H3)
 206               |apply primeb_true_to_prime.
 207                apply (andb_true_true ? ? H5)
 208               |assumption
 209               ]
 210             ]
 211           |apply lt_O_ord_rem
 212             [apply prime_to_lt_SO.
 213              apply primeb_true_to_prime.
 214              apply (andb_true_true ? ? H3)
 215             |assumption
 216             ]
 217           |apply not_eq_to_le_to_lt
 218             [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
 219               [elim H4.
 220                intro.rewrite > H7 in H6.simplify in H6.
 221                apply (not_divides_ord_rem m n)
 222                 [assumption
 223                 |apply prime_to_lt_SO.
 224                  apply primeb_true_to_prime.
 225                  apply (andb_true_true ? ? H3)
 226                 |apply divides_b_true_to_divides.
 227                  apply (andb_true_true_r ? ? H6)
 228                 ]
 229               |elim H4.rewrite > H6.
 230                apply lt_to_not_eq.
 231                apply prime_to_lt_O.
 232                apply primeb_true_to_prime.
 233                apply (andb_true_true ? ? H3)
 234               ]
 235             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
 236               [apply le_to_le_max.
 237                apply divides_to_le
 238                 [assumption
 239                 |apply divides_ord_rem
 240                   [apply prime_to_lt_SO.
 241                    apply primeb_true_to_prime.
 242                    apply (andb_true_true ? ? H3)
 243                   |assumption
 244                   ]
 245                 ]
 246               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
 247                 [apply le_max_f_max_g.
 248                  intros.
 249                  apply (bool_elim ? (primeb i));intro
 250                   [simplify.
 251                    apply divides_to_divides_b_true
 252                     [apply prime_to_lt_O.
 253                      apply primeb_true_to_prime.
 254                      assumption
 255                     |apply (trans_divides ? (ord_rem m n))
 256                       [apply divides_b_true_to_divides.
 257                        apply (andb_true_true_r ? ? H5)
 258                       |apply divides_ord_rem
 259                         [apply prime_to_lt_SO.
 260                          apply primeb_true_to_prime.
 261                          apply (andb_true_true ? ? H3)
 262                         |assumption
 263                         ]
 264                       ]
 265                     ]
 266                   |rewrite > H6 in H5.
 267                    assumption
 268                   ]
 269                 |apply le_S_S_to_le.
 270                  assumption
 271                 ]
 272               ]
 273             ]
 274           ]
 275         |apply prime_to_lt_SO.
 276          apply primeb_true_to_prime.
 277          apply (andb_true_true ? ? H3)
 278         |assumption
 279         ]
 280       |assumption
 281       ]
 282     |elim (le_to_or_lt_eq ? ? H1)
 283       [rewrite > false_to_pi_p_Sn
 284         [apply H
 285           [assumption
 286           |apply false_to_lt_max
 287             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
 288               [apply lt_to_le.
 289                apply lt_SO_max_prime.
 290                assumption
 291               |apply le_S_S_to_le.
 292                assumption
 293               ]
 294             |assumption
 295             |apply le_S_S_to_le.
 296              assumption
 297             ]
 298           ]
 299         |assumption
 300         ]
 301       |rewrite < H4.
 302        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
 303        apply eq_pi_p
 304         [intros.
 305          apply (bool_elim ? (primeb x));intro
 306           [apply sym_eq.
 307            change with (divides_b x (S O) =false).
 308            apply not_divides_to_divides_b_false
 309             [apply prime_to_lt_O.
 310              apply primeb_true_to_prime.
 311              assumption
 312             |intro.
 313              apply (le_to_not_lt x (S O))
 314               [apply divides_to_le
 315                 [apply lt_O_S.assumption
 316                 |assumption
 317                 ]
 318               |elim (primeb_true_to_prime ? H6).
 319                assumption
 320               ]
 321             ]
 322           |reflexivity
 323           ]
 324         |intros.reflexivity
 325         ]
 326       ]
 327     ]
 328   ]
 329 qed.
 330
 331 (* factorization of n into primes *)
 332 theorem pi_p_primeb_divides_b: \forall n. O < n \to
 333 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 334 intros.
 335 apply lt_max_to_pi_p_primeb
 336   [assumption
 337   |apply le_S_S.
 338    apply le_max_n
 339   ]
 340 qed.
 341
 342 theorem pi_p_primeb: \forall n. O < n \to
 343 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
 344 intros.
 345 rewrite < eq_pi_p_primeb_divides_b.
 346 apply pi_p_primeb_divides_b.
 347 assumption.
 348 qed.
 349
 350 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
 351 ord n p \le log p n.
 352 intros.
 353 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
 354   [rewrite > log_exp
 355     [apply le_plus_n_r
 356     |assumption
 357     |apply lt_O_ord_rem;assumption
 358     ]
 359   |assumption
 360   |assumption
 361   ]
 362 qed.
 363
 364 theorem sigma_p_divides_b:
 365 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
 366 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 367 intro.elim m
 368   [reflexivity
 369   |simplify in ⊢ (? ? ? (? % ? ?)).
 370    rewrite > true_to_sigma_p_Sn
 371     [rewrite > sym_plus.rewrite < plus_n_SO.
 372      apply eq_f.
 373      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
 374      apply eq_sigma_p1
 375       [intros.
 376        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
 377         [apply sym_eq.
 378          apply divides_to_divides_b_true
 379           [apply lt_O_exp.
 380            apply prime_to_lt_O.
 381            assumption
 382           |apply (witness ? ? ((exp p (n - x))*n1)).
 383            rewrite < assoc_times.
 384            rewrite < exp_plus_times.
 385            apply eq_f2
 386             [apply eq_f.simplify.
 387              apply eq_f.
 388              rewrite > sym_plus.
 389              apply plus_minus_m_m.
 390              apply lt_to_le.assumption
 391             |reflexivity
 392             ]
 393           ]
 394         |apply sym_eq.
 395          apply False_ind.
 396          apply (divides_b_false_to_not_divides ? ? H5).
 397          apply (witness ? ? ((exp p (n - S x))*n1)).
 398          rewrite < assoc_times.
 399          rewrite < exp_plus_times.
 400          apply eq_f2
 401           [apply eq_f.
 402            rewrite > sym_plus.
 403            apply plus_minus_m_m.
 404            assumption
 405           |reflexivity
 406           ]
 407         ]
 408       |intros.reflexivity
 409       ]
 410     |apply divides_to_divides_b_true
 411       [apply lt_O_exp.
 412        apply prime_to_lt_O.assumption
 413       |apply (witness ? ? n1).reflexivity
 414       ]
 415     ]
 416   ]
 417 qed.
 418
 419 theorem sigma_p_divides_b1:
 420 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
 421 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 422 intros.
 423 lapply (prime_to_lt_SO ? H1) as H4.
 424 lapply (prime_to_lt_O ? H1) as H5.
 425 rewrite > (false_to_eq_sigma_p m k)
 426   [apply sigma_p_divides_b;assumption
 427   |assumption
 428   |intros.
 429    apply not_divides_to_divides_b_false
 430     [apply lt_O_exp.assumption
 431     |intro.apply (le_to_not_lt ? ? H6).
 432      unfold lt.
 433      rewrite < (ord_exp p)
 434       [rewrite > (plus_n_O m).
 435        rewrite < (not_divides_to_ord_O ? ? H1 H2).
 436        rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
 437        rewrite < ord_times
 438         [apply divides_to_le_ord
 439           [apply lt_O_exp.assumption
 440           |rewrite > (times_n_O O).
 441            apply lt_times
 442             [apply lt_O_exp.assumption
 443             |assumption
 444             ]
 445           |assumption
 446           |assumption
 447           ]
 448         |apply lt_O_exp.assumption
 449         |assumption
 450         |assumption
 451         ]
 452       |assumption
 453       ]
 454     ]
 455   ]
 456 qed.
 457
 458 theorem eq_ord_sigma_p:
 459 \forall n,m,x. O < n \to prime x \to
 460 exp x m \le n \to n < exp x (S m) \to
 461 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
 462 intros.
 463 lapply (prime_to_lt_SO ? H1).
 464 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
 465   [apply sigma_p_divides_b1
 466     [apply lt_O_ord_rem;assumption
 467     |assumption
 468     |apply not_divides_ord_rem;assumption
 469     |apply lt_S_to_le.
 470      apply (le_to_lt_to_lt ? (log x n))
 471       [apply le_ord_log;assumption
 472       |apply (lt_exp_to_lt x)
 473         [assumption
 474         |apply (le_to_lt_to_lt ? n ? ? H3).
 475          apply le_exp_log.
 476          assumption
 477         ]
 478       ]
 479     ]
 480   |assumption
 481   |assumption
 482   ]
 483 qed.
 484
 485 theorem pi_p_primeb1: \forall n. O < n \to
 486 n = pi_p (S n) primeb
 487   (\lambda p.(pi_p (log p n)
 488     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
 489 intros.
 490 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
 491 apply eq_pi_p1
 492   [intros.reflexivity
 493   |intros.
 494    rewrite > exp_sigma_p.
 495    apply eq_f.
 496    apply eq_ord_sigma_p
 497     [assumption
 498     |apply primeb_true_to_prime.
 499      assumption
 500     |apply le_exp_log.assumption
 501     |apply lt_exp_log.
 502      apply prime_to_lt_SO.
 503      apply primeb_true_to_prime.
 504      assumption
 505     ]
 506   ]
 507 qed.
 508
 509 (* the factorial function *)
 510 theorem eq_fact_pi_p:\forall n. fact n =
 511 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 512 intro.elim n
 513   [reflexivity
 514   |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
 515    rewrite > true_to_pi_p_Sn
 516     [apply eq_f.assumption
 517     |reflexivity
 518     ]
 519   ]
 520 qed.
 521
 522 theorem eq_sigma_p_div: \forall n,q.O < q \to
 523 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
 524 =n/q.
 525 intros.
 526 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 527   [apply div_mod_spec_intro
 528     [apply lt_mod_m_m.assumption
 529     |elim n
 530       [simplify.elim q;reflexivity
 531       |elim (or_div_mod1 n1 q)
 532         [elim H2.clear H2.
 533          rewrite > divides_to_mod_O
 534           [rewrite < plus_n_O.
 535            rewrite > true_to_sigma_p_Sn
 536             [rewrite > H4 in ⊢ (? ? % ?).
 537              apply eq_f2
 538               [rewrite < sym_plus.
 539                rewrite < plus_n_SO.
 540                apply eq_f.
 541                apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 542                 [apply div_mod_spec_div_mod.
 543                  assumption
 544                 |apply div_mod_spec_intro
 545                   [apply lt_mod_m_m.assumption
 546                   |assumption
 547                   ]
 548                 ]
 549               |reflexivity
 550               ]
 551             |apply true_to_true_to_andb_true
 552               [reflexivity
 553               |apply divides_to_divides_b_true;assumption
 554               ]
 555             ]
 556           |assumption
 557           |assumption
 558           ]
 559         |elim H2.clear H2.
 560          rewrite > false_to_sigma_p_Sn
 561           [rewrite > mod_S
 562             [rewrite < plus_n_Sm.
 563              apply eq_f.
 564              assumption
 565             |assumption
 566             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
 567               [assumption
 568               |apply False_ind.
 569                apply H3.
 570                apply (witness ? ? (S(div n1 q))).
 571                rewrite < times_n_Sm.
 572                rewrite < sym_plus.
 573                rewrite < H2 in ⊢ (? ? ? (? ? %)).
 574                rewrite > sym_times.
 575                assumption
 576               |apply lt_mod_m_m.
 577                assumption
 578               ]
 579             ]
 580           |rewrite > not_divides_to_divides_b_false
 581             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
 582             |assumption
 583             |assumption
 584             ]
 585           ]
 586         |assumption
 587         ]
 588       ]
 589     ]
 590   |apply div_mod_spec_div_mod.
 591    assumption
 592   ]
 593 qed.
 594
 595 (* still another characterization of the factorial *)
 596 theorem fact_pi_p: \forall n. fact n =
 597 pi_p (S n) primeb
 598   (\lambda p.(pi_p (log p n)
 599     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
 600 intros.
 601 rewrite > eq_fact_pi_p.
 602 apply (trans_eq ? ?
 603   (pi_p (S n) (λi:nat.leb (S O) i)
 604    (λn.pi_p (S n) primeb
 605     (\lambda p.(pi_p (log p n)
 606      (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
 607   [apply eq_pi_p1;intros
 608     [reflexivity
 609     |apply pi_p_primeb1.
 610      apply leb_true_to_le.assumption
 611     ]
 612   |apply (trans_eq ? ?
 613     (pi_p (S n) (λi:nat.leb (S O) i)
 614      (λn:nat
 615       .pi_p (S n) (\lambda p.primeb p\land leb p n)
 616        (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
 617     [apply eq_pi_p1
 618       [intros.reflexivity
 619       |intros.apply eq_pi_p1
 620         [intros.elim (primeb x1)
 621           [simplify.apply sym_eq.
 622            apply le_to_leb_true.
 623            apply le_S_S_to_le.
 624            assumption
 625           |reflexivity
 626           ]
 627         |intros.reflexivity
 628         ]
 629       ]
 630     |apply (trans_eq ? ?
 631       (pi_p (S n) (λi:nat.leb (S O) i)
 632        (λm:nat
 633         .pi_p (S n) (λp:nat.primeb p∧leb p m)
 634          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
 635       [apply eq_pi_p1
 636         [intros.reflexivity
 637         |intros.
 638          apply sym_eq.
 639          apply false_to_eq_pi_p
 640           [assumption
 641           |intros.rewrite > lt_to_leb_false
 642             [elim primeb;reflexivity|assumption]
 643           ]
 644         ]
 645       |(* make a general theorem *)
 646        apply (trans_eq ? ?
 647         (pi_p (S n) primeb
 648          (λp:nat
 649           .pi_p (S n) (λm.leb p m)
 650            (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
 651         ))
 652         [apply pi_p_pi_p1.
 653          intros.
 654          apply (bool_elim ? (primeb y \land leb y x));intros
 655           [rewrite > (le_to_leb_true (S O) x)
 656             [reflexivity
 657             |apply (trans_le ? y)
 658               [apply prime_to_lt_O.
 659                apply primeb_true_to_prime.
 660                apply (andb_true_true ? ? H2)
 661               |apply leb_true_to_le.
 662                apply (andb_true_true_r ? ? H2)
 663               ]
 664             ]
 665           |elim (leb (S O) x);reflexivity
 666           ]
 667         |apply eq_pi_p1
 668           [intros.reflexivity
 669           |intros.
 670            apply (trans_eq ? ?
 671             (pi_p (S n) (λm:nat.leb x m)
 672              (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
 673             [apply eq_pi_p1
 674               [intros.reflexivity
 675               |intros.
 676                apply sym_eq.
 677                apply false_to_eq_pi_p
 678                 [apply le_log
 679                   [apply prime_to_lt_SO.
 680                    apply primeb_true_to_prime.
 681                    assumption
 682                   |apply le_S_S_to_le.
 683                    assumption
 684                   ]
 685                 |intros.
 686                  apply not_divides_to_divides_b_false
 687                   [apply lt_O_exp.
 688                    apply prime_to_lt_O.
 689                    apply primeb_true_to_prime.
 690                    assumption
 691                   |intro.
 692                    apply (lt_to_not_le x1 (exp x (S i)))
 693                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
 694                       [apply lt_exp_log.
 695                        apply prime_to_lt_SO.
 696                        apply primeb_true_to_prime.
 697                        assumption
 698                       |apply le_exp
 699                         [apply prime_to_lt_O.
 700                          apply primeb_true_to_prime.
 701                          assumption
 702                         |apply le_S_S.
 703                          assumption
 704                         ]
 705                       ]
 706                     |apply divides_to_le
 707                       [apply (lt_to_le_to_lt ? x)
 708                         [apply prime_to_lt_O.
 709                          apply primeb_true_to_prime.
 710                          assumption
 711                         |apply leb_true_to_le.
 712                          assumption
 713                         ]
 714                       |assumption
 715                       ]
 716                     ]
 717                   ]
 718                 ]
 719               ]
 720             |apply
 721              (trans_eq ? ?
 722               (pi_p (log x n) (λi:nat.true)
 723                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
 724               [apply (pi_p_pi_p1 (\lambda m,i.x)).
 725                intros.
 726                reflexivity
 727               |apply eq_pi_p1
 728                 [intros.reflexivity
 729                 |intros.
 730                  rewrite > exp_sigma_p.
 731                  apply eq_f.
 732                  apply (trans_eq ? ?
 733                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
 734                   [apply eq_sigma_p1
 735                     [intros.
 736                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
 737                       [apply (bool_elim ? (leb x x2));intro
 738                         [rewrite > le_to_leb_true
 739                           [reflexivity
 740                           |apply (trans_le ? x)
 741                             [apply prime_to_lt_O.
 742                              apply primeb_true_to_prime.
 743                              assumption
 744                             |apply leb_true_to_le.
 745                              assumption
 746                             ]
 747                           ]
 748                         |rewrite > lt_to_leb_false
 749                           [reflexivity
 750                           |apply not_le_to_lt.intro.
 751                            apply (leb_false_to_not_le ? ? H6).
 752                            apply (trans_le ? (exp x (S x1)))
 753                             [rewrite > times_n_SO in ⊢ (? % ?).
 754                              change with (exp x (S O) \le exp x (S x1)).
 755                              apply le_exp
 756                               [apply prime_to_lt_O.
 757                                apply primeb_true_to_prime.
 758                                assumption
 759                               |apply le_S_S.apply le_O_n.
 760                               ]
 761                             |apply divides_to_le
 762                               [assumption
 763                               |apply divides_b_true_to_divides.
 764                                assumption
 765                               ]
 766                             ]
 767                           ]
 768                         ]
 769                       |rewrite < andb_sym.
 770                        rewrite < andb_sym in ⊢ (? ? ? %).
 771                        reflexivity
 772                       ]
 773                     |intros.reflexivity
 774                     ]
 775                   |apply eq_sigma_p_div.
 776                    apply lt_O_exp.
 777                    apply prime_to_lt_O.
 778                    apply primeb_true_to_prime.
 779                    assumption
 780                   ]
 781                 ]
 782               ]
 783             ]
 784           ]
 785         ]
 786       ]
 787     ]
 788   ]
 789 qed.
 790
 791 (* odd n is just mod n (S(S O))
 792 let rec odd n \def
 793   match n with
 794   [ O \Rightarrow O
 795   | S m \Rightarrow (S O) - odd m
 796   ].
 797
 798 theorem le_odd_SO: \forall n. odd n \le S O.
 799 intro.elim n
 800   [apply le_O_n
 801   |simplify.cases (odd n1)
 802     [simplify.apply le_n.
 803     |apply le_O_n
 804     ]
 805   ]
 806 qed.
 807
 808 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
 809 intro.elim n
 810   [apply (lt_O_n_elim ? H).
 811    intro.simplify.reflexivity
 812   |
 813 *)
 814
 815 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
 816 pi_p (S ((S(S O))*n)) primeb
 817   (\lambda p.(pi_p (log p ((S(S O))*n))
 818     (\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)))))))).
 819 intros.rewrite > fact_pi_p.
 820 apply eq_pi_p1
 821   [intros.reflexivity
 822   |intros.apply eq_pi_p
 823     [intros.reflexivity
 824     |intros.
 825      rewrite < exp_plus_times.
 826      apply eq_f.
 827      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 828      apply SSO_mod.
 829      apply lt_O_exp.
 830      apply prime_to_lt_O.
 831      apply primeb_true_to_prime.
 832      assumption
 833     ]
 834   ]
 835 qed.
 836
 837 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
 838 pi_p (S ((S(S O))*n)) primeb
 839   (\lambda p.(pi_p (log p ((S(S O))*n))
 840     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
 841 pi_p (S ((S(S O))*n)) primeb
 842   (\lambda p.(pi_p (log p ((S(S O))*n))
 843     (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
 844 intros.
 845 rewrite < times_pi_p.
 846 rewrite > fact_pi_p2.
 847 apply eq_pi_p;intros
 848   [reflexivity
 849   |apply times_pi_p
 850   ]
 851 qed.
 852
 853 theorem pi_p_primeb4: \forall n. S O < n \to
 854 pi_p (S ((S(S O))*n)) primeb
 855   (\lambda p.(pi_p (log p ((S(S O))*n))
 856     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 857 =
 858 pi_p (S n) primeb
 859   (\lambda p.(pi_p (log p (S(S O)*n))
 860     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 861 intros.
 862 apply or_false_eq_SO_to_eq_pi_p
 863   [apply le_S_S.
 864    apply le_times_n.
 865    apply lt_O_S
 866   |intros.
 867    right.
 868    rewrite > log_i_SSOn
 869     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
 870      rewrite < times_n_SO.
 871      rewrite > eq_div_O
 872       [reflexivity
 873       |simplify.rewrite < times_n_SO.assumption
 874       ]
 875     |assumption
 876     |assumption
 877     |apply le_S_S_to_le.assumption
 878     ]
 879   ]
 880 qed.
 881
 882 theorem pi_p_primeb5: \forall n. S O < n \to
 883 pi_p (S ((S(S O))*n)) primeb
 884   (\lambda p.(pi_p (log p ((S(S O))*n))
 885     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 886 =
 887 pi_p (S n) primeb
 888   (\lambda p.(pi_p (log p n)
 889     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 890 intros.
 891 rewrite > (pi_p_primeb4 ? H).
 892 apply eq_pi_p1;intros
 893   [reflexivity
 894   |apply or_false_eq_SO_to_eq_pi_p
 895     [apply le_log
 896       [apply prime_to_lt_SO.
 897        apply primeb_true_to_prime.
 898        assumption
 899       |apply le_times_n.
 900        apply lt_O_S
 901       ]
 902     |intros.right.
 903      rewrite > eq_div_O
 904       [simplify.reflexivity
 905       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
 906         [apply lt_exp_log.
 907          apply prime_to_lt_SO.
 908          apply primeb_true_to_prime.
 909          assumption
 910         |apply le_exp
 911           [apply prime_to_lt_O.
 912            apply primeb_true_to_prime.
 913            assumption
 914           |apply le_S_S.
 915            assumption
 916           ]
 917         ]
 918       ]
 919     ]
 920   ]
 921 qed.
 922
 923 theorem exp_fact_SSO: \forall n.
 924 exp (fact n) (S(S O))
 925 =
 926 pi_p (S n) primeb
 927   (\lambda p.(pi_p (log p n)
 928     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 929 intros.
 930 rewrite > fact_pi_p.
 931 rewrite < exp_pi_p.
 932 apply eq_pi_p;intros
 933   [reflexivity
 934   |apply sym_eq.
 935    apply exp_times_pi_p
 936   ]
 937 qed.
 938
 939 definition B \def
 940 \lambda n.
 941 pi_p (S n) primeb
 942   (\lambda p.(pi_p (log p n)
 943     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 944
 945 theorem B_SSSO: B 3 = 6.
 946 reflexivity.
 947 qed.
 948
 949 theorem B_SSSSO: B 4 = 6.
 950 reflexivity.
 951 qed.
 952
 953 theorem B_SSSSSO: B 5 = 30.
 954 reflexivity.
 955 qed.
 956
 957 theorem B_SSSSSSO: B 6 = 20.
 958 reflexivity.
 959 qed.
 960
 961 theorem B_SSSSSSSO: B 7 = 140.
 962 reflexivity.
 963 qed.
 964
 965 theorem B_SSSSSSSSO: B 8 = 70.
 966 reflexivity.
 967 qed.
 968
 969 theorem eq_fact_B:\forall n.S O < n \to
 970 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 971 intros. unfold B.
 972 rewrite > fact_pi_p3.
 973 apply eq_f2
 974   [apply sym_eq.
 975    rewrite > pi_p_primeb5
 976     [apply exp_fact_SSO
 977     |assumption
 978     ]
 979   |reflexivity
 980   ]
 981 qed.
 982
 983 theorem le_B_A: \forall n. B n \le A n.
 984 intro.unfold B.
 985 rewrite > eq_A_A'.
 986 unfold A'.
 987 apply le_pi_p.intros.
 988 apply le_pi_p.intros.
 989 rewrite > exp_n_SO in ⊢ (? ? %).
 990 apply le_exp
 991   [apply prime_to_lt_O.
 992    apply primeb_true_to_prime.
 993    assumption
 994   |apply le_S_S_to_le.
 995    apply lt_mod_m_m.
 996    apply lt_O_S
 997   ]
 998 qed.
 999
1000 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).
1001 intros.unfold B.
1002 rewrite > eq_A_A'.
1003 unfold A'.
1004 cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
1005   [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
1006     [rewrite > (pi_p_gi ? ? (S(S O)))
1007       [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
1008         [rewrite < assoc_times.
1009          apply le_times
1010           [rewrite > (pi_p_gi ? ? O)
1011             [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
1012               [rewrite < assoc_times.
1013                apply le_times
1014                 [rewrite < exp_n_SO.
1015                  change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
1016                  with ((S(S O))*(S(S O))).
1017                  rewrite > assoc_times.
1018                  rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
1019                  rewrite > lt_O_to_div_times
1020                   [rewrite > divides_to_mod_O
1021                     [apply le_n
1022                     |apply lt_O_S
1023                     |apply (witness ? ? n).reflexivity
1024                     ]
1025                   |apply lt_O_S
1026                   ]
1027                 |apply le_pi_p.intros.
1028                  rewrite > exp_n_SO in ⊢ (? ? %).
1029                  apply le_exp
1030                   [apply lt_O_S
1031                   |apply le_S_S_to_le.
1032                    apply lt_mod_m_m.
1033                    apply lt_O_S
1034                   ]
1035                 ]
1036               |assumption
1037               |reflexivity
1038               ]
1039             |assumption
1040             |reflexivity
1041             ]
1042           |apply le_pi_p.intros.
1043            apply le_pi_p.intros.
1044            rewrite > exp_n_SO in ⊢ (? ? %).
1045            apply le_exp
1046             [apply prime_to_lt_O.
1047              apply primeb_true_to_prime.
1048              apply (andb_true_true ? ? H2)
1049             |apply le_S_S_to_le.
1050              apply lt_mod_m_m.
1051              apply lt_O_S
1052             ]
1053           ]
1054         |assumption
1055         |reflexivity
1056         ]
1057       |assumption
1058       |reflexivity
1059       ]
1060     |apply lt_O_log
1061       [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
1062        apply lt_times_r1
1063         [apply lt_O_S
1064         |assumption
1065         ]
1066       |rewrite > times_n_SO in ⊢ (? % ?).
1067        apply le_times
1068         [apply le_S.apply le_S.apply le_n
1069         |assumption
1070         ]
1071       ]
1072     ]
1073   |apply le_S_S.
1074    rewrite > times_n_SO in ⊢ (? % ?).
1075    apply le_times
1076     [apply le_S.apply le_n_Sn
1077     |assumption
1078     ]
1079   ]
1080 qed.
1081
1082 theorem le_fact_A:\forall n.S O < n \to
1083 fact (2*n) \le exp (fact n) 2 * A (2*n).
1084 intros.
1085 rewrite > eq_fact_B
1086   [apply le_times_r.
1087    apply le_B_A
1088   |assumption
1089   ]
1090 qed.
1091
1092 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1093 B (2*n) \le exp 2 (pred (2*n)).
1094 intros.
1095 apply (le_times_to_le (exp (fact n) (S(S O))))
1096   [apply lt_O_exp.
1097    apply lt_O_fact
1098   |rewrite < eq_fact_B
1099     [rewrite < sym_times in ⊢ (? ? %).
1100      rewrite > exp_SSO.
1101      rewrite < assoc_times.
1102      apply fact1
1103     |assumption
1104     ]
1105   ]
1106 qed.
1107
1108 theorem le_B_exp: \forall n.
1109 B (2*n) \le exp 2 (pred (2*n)).
1110 intro.cases n
1111   [apply le_n
1112   |cases n1
1113     [simplify.apply le_n
1114     |apply lt_SO_to_le_B_exp.
1115      apply le_S_S.apply lt_O_S.
1116     ]
1117   ]
1118 qed.
1119
1120 theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
1121 B (2*n) \le exp 2 ((2*n)-2).
1122 intros.
1123 apply (le_times_to_le (exp (fact n) (S(S O))))
1124   [apply lt_O_exp.
1125    apply lt_O_fact
1126   |rewrite < eq_fact_B
1127     [rewrite < sym_times in ⊢ (? ? %).
1128      rewrite > exp_SSO.
1129      rewrite < assoc_times.
1130      apply lt_SSSSO_to_fact.assumption
1131     |apply lt_to_le.apply lt_to_le.
1132      apply lt_to_le.assumption
1133     ]
1134   ]
1135 qed.
1136
1137 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1138 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1139 intros.
1140 apply (le_times_to_le (exp (fact n) (S(S O))))
1141   [apply lt_O_exp.
1142    apply lt_O_fact
1143   |rewrite < assoc_times in ⊢ (? ? %).
1144    rewrite > sym_times in ⊢ (? ? (? % ?)).
1145    rewrite > assoc_times in ⊢ (? ? %).
1146    rewrite < eq_fact_B
1147     [rewrite < sym_times.
1148      apply fact3.
1149      apply lt_to_le.assumption
1150     |assumption
1151     ]
1152   ]
1153 qed.
1154
1155 theorem le_exp_B: \forall n. O < n \to
1156 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1157 intros.
1158 elim H
1159   [apply le_n
1160   |apply lt_SO_to_le_exp_B.
1161    apply le_S_S.assumption
1162   ]
1163 qed.
1164
1165 theorem eq_A_SSO_n: \forall n.O < n \to
1166 A((S(S O))*n) =
1167  pi_p (S ((S(S O))*n)) primeb
1168   (\lambda p.(pi_p (log p ((S(S O))*n) )
1169     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1170  *A n.
1171 intro.
1172 rewrite > eq_A_A'.rewrite > eq_A_A'.
1173 unfold A'.intros.
1174 cut (
1175  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1176  = pi_p (S ((S(S O))*n)) primeb
1177     (λ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))))))))
1178   [rewrite > Hcut.
1179    rewrite < times_pi_p.
1180    apply eq_pi_p1;intros
1181     [reflexivity
1182     |rewrite < times_pi_p.
1183      apply eq_pi_p;intros
1184       [reflexivity
1185       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1186         [simplify.rewrite < times_n_SO.apply times_n_SO
1187         |simplify.rewrite < plus_n_O.apply times_n_SO
1188         ]
1189       ]
1190     ]
1191   |apply (trans_eq ? ? (pi_p (S n) primeb
1192     (\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))))))))
1193     [apply eq_pi_p1;intros
1194       [reflexivity
1195       |apply eq_pi_p1;intros
1196         [reflexivity
1197         |rewrite > lt_to_leb_false
1198           [simplify.apply times_n_SO
1199           |apply le_S_S.
1200            apply (trans_le ? (exp x (log x n)))
1201             [apply le_exp
1202               [apply prime_to_lt_O.
1203                apply primeb_true_to_prime.
1204                assumption
1205               |assumption
1206               ]
1207             |apply le_exp_log.
1208              assumption
1209             ]
1210           ]
1211         ]
1212       ]
1213     |apply (trans_eq ? ?
1214       (pi_p (S ((S(S O))*n)) primeb
1215        (λp:nat.pi_p (log p n) (λi:nat.true)
1216         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1217       [apply sym_eq.
1218        apply or_false_eq_SO_to_eq_pi_p
1219         [apply le_S_S.
1220          simplify.
1221          apply le_plus_n_r
1222         |intros.right.
1223          rewrite > lt_to_log_O
1224           [reflexivity
1225           |assumption
1226           |assumption
1227           ]
1228         ]
1229       |apply eq_pi_p1;intros
1230         [reflexivity
1231         |apply sym_eq.
1232          apply or_false_eq_SO_to_eq_pi_p
1233           [apply le_log
1234             [apply prime_to_lt_SO.
1235              apply primeb_true_to_prime.
1236              assumption
1237             |simplify.
1238              apply le_plus_n_r
1239             ]
1240           |intros.right.
1241            rewrite > le_to_leb_true
1242             [simplify.reflexivity
1243             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1244               [apply lt_exp_log.
1245                apply prime_to_lt_SO.
1246                apply primeb_true_to_prime.
1247                assumption
1248               |apply le_exp
1249                 [apply prime_to_lt_O.
1250                  apply primeb_true_to_prime.
1251                  assumption
1252                 |apply le_S_S.assumption
1253                 ]
1254               ]
1255             ]
1256           ]
1257         ]
1258       ]
1259     ]
1260   ]
1261 qed.
1262
1263 theorem le_A_BA1: \forall n. O < n \to
1264 A((S(S O))*n) \le B((S(S O))*n)*A n.
1265 intros.
1266 rewrite > eq_A_SSO_n
1267   [apply le_times_l.
1268    unfold B.
1269    apply le_pi_p.intros.
1270    apply le_pi_p.intros.
1271    apply le_exp
1272     [apply prime_to_lt_O.
1273      apply primeb_true_to_prime.
1274      assumption
1275     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1276       [simplify in ⊢ (? % ?).
1277        cut ((S(S O))*n/i\sup(S i1) = S O)
1278         [rewrite > Hcut.apply le_n
1279         |apply (div_mod_spec_to_eq
1280           ((S(S O))*n) (exp i (S i1))
1281            ? (mod ((S(S O))*n) (exp i (S i1)))
1282            ? (minus ((S(S O))*n) (exp i (S i1))) )
1283           [apply div_mod_spec_div_mod.
1284            apply lt_O_exp.
1285            apply prime_to_lt_O.
1286            apply primeb_true_to_prime.
1287            assumption
1288           |cut (i\sup(S i1)≤(S(S O))*n)
1289             [apply div_mod_spec_intro
1290               [apply lt_plus_to_lt_minus
1291                 [assumption
1292                 |simplify in ⊢ (? % ?).
1293                  rewrite < plus_n_O.
1294                  apply lt_plus
1295                   [apply leb_true_to_le.assumption
1296                   |apply leb_true_to_le.assumption
1297                   ]
1298                 ]
1299               |rewrite > sym_plus.
1300                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1301                rewrite < times_n_SO.
1302                apply plus_minus_m_m.
1303                assumption
1304               ]
1305             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1306               [apply le_exp
1307                 [apply prime_to_lt_O.
1308                  apply primeb_true_to_prime.
1309                  assumption
1310                 |assumption
1311                 ]
1312               |apply le_exp_log.
1313                rewrite > (times_n_O O) in ⊢ (? % ?).
1314                apply lt_times
1315                 [apply lt_O_S
1316                 |assumption
1317                 ]
1318               ]
1319             ]
1320           ]
1321         ]
1322       |apply le_O_n
1323       ]
1324     ]
1325   |assumption
1326   ]
1327 qed.
1328
1329 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1330 intros.cases n
1331   [apply le_n
1332   |apply le_A_BA1.apply lt_O_S
1333   ]
1334 qed.
1335
1336 theorem le_A_exp: \forall n.
1337 A(2*n) \le (exp 2 (pred (2*n)))*A n.
1338 intro.
1339 apply (trans_le ? (B(2*n)*A n))
1340   [apply le_A_BA
1341   |apply le_times_l.
1342    apply le_B_exp
1343   ]
1344 qed.
1345
1346 theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
1347 A(2*n) \le exp 2 ((2*n)-2)*A n.
1348 intros.
1349 apply (trans_le ? (B(2*n)*A n))
1350   [apply le_A_BA
1351   |apply le_times_l.
1352    apply lt_SSSSO_to_le_B_exp.assumption
1353   ]
1354 qed.
1355
1356 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1357 intro.cases n
1358   [apply le_n
1359   |simplify.apply le_plus_r.
1360    apply le_n_Sn
1361   ]
1362 qed.
1363
1364 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1365 intros.
1366 elim H
1367   [apply le_n
1368   |rewrite > times_SSO.
1369    apply le_S_S.
1370    apply (trans_le ? (2*n1))
1371     [assumption
1372     |apply le_n_Sn
1373     ]
1374   ]
1375 qed.
1376
1377 theorem le_A_exp1: \forall n.
1378 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1379 intro.elim n
1380   [simplify.apply le_n
1381   |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1382    apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1383     [apply le_A_exp
1384     |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1385       [apply le_times_r.
1386        assumption
1387       |rewrite < exp_plus_times.
1388        apply le_exp
1389         [apply lt_O_S
1390         |cut (S(S n1) \le 2*(exp 2 n1))
1391           [apply le_S_S_to_le.
1392            change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1393            rewrite < S_pred
1394             [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1395              rewrite < S_pred
1396               [rewrite < eq_minus_plus_plus_minus
1397                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1398                  apply le_n
1399                 |assumption
1400                 ]
1401               |apply lt_to_lt_O_minus.
1402                apply (lt_to_le_to_lt ? (2*(S(S n1))))
1403                 [rewrite > times_n_SO in ⊢ (? % ?).
1404                  rewrite > sym_times.
1405                  apply lt_times_l1
1406                   [apply lt_O_S
1407                   |apply le_n
1408                   ]
1409                 |apply le_times_r.
1410                  assumption
1411                 ]
1412               ]
1413             |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1414              apply le_times
1415               [apply le_n_Sn
1416               |apply lt_O_exp.
1417                apply lt_O_S
1418               ]
1419             ]
1420           |elim n1
1421             [apply le_n
1422             |apply (trans_le ? (2*(S(S n2))))
1423               [apply le_S_times_SSO.
1424                apply lt_O_S
1425               |apply le_times_r.
1426                assumption
1427               ]
1428             ]
1429           ]
1430         ]
1431       ]
1432     ]
1433   ]
1434 qed.
1435
1436 theorem monotonic_A: monotonic nat le A.
1437 unfold.intros.
1438 elim H
1439   [apply le_n
1440   |apply (trans_le ? (A n1))
1441     [assumption
1442     |unfold A.
1443      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1444           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1445       [apply (bool_elim ? (primeb (S n1)));intro
1446         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1447          rewrite > times_n_SO in ⊢ (? % ?).
1448          rewrite > sym_times.
1449          apply le_times
1450           [apply lt_O_exp.apply lt_O_S
1451           |assumption
1452           ]
1453         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1454          assumption
1455         ]
1456       |apply le_pi_p.intros.
1457        apply le_exp
1458         [apply prime_to_lt_O.
1459          apply primeb_true_to_prime.
1460          assumption
1461         |apply le_log
1462           [apply prime_to_lt_SO.
1463            apply primeb_true_to_prime.
1464            assumption
1465           |apply le_S.apply le_n
1466           ]
1467         ]
1468       ]
1469     ]
1470   ]
1471 qed.
1472
1473 (*
1474 theorem le_A_exp2: \forall n. O < n \to
1475 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1476 intros.
1477 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1478   [apply monotonic_A.
1479    apply lt_to_le.
1480    apply lt_exp_log.
1481    apply le_n
1482   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1483     [apply le_A_exp1
1484     |apply le_exp
1485       [apply lt_O_S
1486       |rewrite > assoc_times.apply le_times_r.
1487        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1488        apply le_times_r.
1489        apply le_exp_log.
1490        assumption
1491       ]
1492     ]
1493   ]
1494 qed.
1495 *)
1496
1497 (* example *)
1498 theorem A_SO: A (S O) = S O.
1499 reflexivity.
1500 qed.
1501
1502 theorem A_SSO: A (S(S O)) = S (S O).
1503 reflexivity.
1504 qed.
1505
1506 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1507 reflexivity.
1508 qed.
1509
1510 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1511 reflexivity.
1512 qed.
1513
1514 (* da spostare *)
1515 theorem or_eq_eq_S: \forall n.\exists m.
1516 n = (S(S O))*m \lor n = S ((S(S O))*m).
1517 intro.elim n
1518   [apply (ex_intro ? ? O).
1519    left.reflexivity
1520   |elim H.elim H1
1521     [apply (ex_intro ? ? a).
1522      right.apply eq_f.assumption
1523     |apply (ex_intro ? ? (S a)).
1524      left.rewrite > H2.
1525      apply sym_eq.
1526      apply times_SSO
1527     ]
1528   ]
1529 qed.
1530
1531 (*
1532 (* a better result *)
1533 theorem le_A_exp3: \forall n. S O < n \to
1534 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1535 intro.
1536 apply (nat_elim1 n).
1537 intros.
1538 elim (or_eq_eq_S m).
1539 elim H2
1540   [elim (le_to_or_lt_eq (S O) a)
1541     [rewrite > H3 in ⊢ (? % ?).
1542      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1543       [apply le_A_exp
1544       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1545          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1546         [apply le_times_r.
1547          apply H
1548           [rewrite > H3.
1549            rewrite > times_n_SO in ⊢ (? % ?).
1550            rewrite > sym_times.
1551            apply lt_times_l1
1552             [apply lt_to_le.assumption
1553             |apply le_n
1554             ]
1555           |assumption
1556           ]
1557         |rewrite > sym_times.
1558          rewrite > assoc_times.
1559          rewrite < exp_plus_times.
1560          apply (trans_le ?
1561           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1562           [rewrite > assoc_times.
1563            apply le_times_r.
1564            rewrite < exp_plus_times.
1565            apply le_exp
1566             [apply lt_O_S
1567             |rewrite < H3.
1568              simplify.
1569              rewrite < plus_n_O.
1570              apply le_S.apply le_S.
1571              apply le_n
1572             ]
1573           |apply le_times_l.
1574            rewrite > times_exp.
1575            apply monotonic_exp1.
1576            rewrite > H3.
1577            rewrite > sym_times.
1578            cases a
1579             [apply le_n
1580             |simplify.
1581              rewrite < plus_n_Sm.
1582              apply le_S.
1583              apply le_n
1584             ]
1585           ]
1586         ]
1587       ]
1588     |rewrite < H4 in H3.
1589      simplify in H3.
1590      rewrite > H3.
1591      simplify.
1592      apply le_S_S.apply le_S_S.apply le_O_n
1593     |apply not_lt_to_le.intro.
1594      apply (lt_to_not_le ? ? H1).
1595      rewrite > H3.
1596      apply (le_n_O_elim a)
1597       [apply le_S_S_to_le.assumption
1598       |apply le_O_n
1599       ]
1600     ]
1601   |elim (le_to_or_lt_eq O a (le_O_n ?))
1602     [apply (trans_le ? (A ((S(S O))*(S a))))
1603       [apply monotonic_A.
1604        rewrite > H3.
1605        rewrite > times_SSO.
1606        apply le_n_Sn
1607       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1608         [apply le_A_exp
1609         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1610            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1611           [apply le_times_r.
1612            apply H
1613             [rewrite > H3.
1614              apply le_S_S.
1615              simplify.
1616              rewrite > plus_n_SO.
1617              apply le_plus_r.
1618              rewrite < plus_n_O.
1619              assumption
1620             |apply le_S_S.assumption
1621             ]
1622           |rewrite > sym_times.
1623            rewrite > assoc_times.
1624            rewrite < exp_plus_times.
1625            apply (trans_le ?
1626             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1627             [rewrite > assoc_times.
1628              apply le_times_r.
1629              rewrite < exp_plus_times.
1630              apply le_exp
1631               [apply lt_O_S
1632               |rewrite > times_SSO.
1633                rewrite < H3.
1634                simplify.
1635                rewrite < plus_n_Sm.
1636                rewrite < plus_n_O.
1637                apply le_n
1638               ]
1639             |apply le_times_l.
1640              rewrite > times_exp.
1641              apply monotonic_exp1.
1642              rewrite > H3.
1643              rewrite > sym_times.
1644              apply le_n
1645             ]
1646           ]
1647         ]
1648       ]
1649     |rewrite < H4 in H3.simplify in H3.
1650      apply False_ind.
1651      apply (lt_to_not_le ? ? H1).
1652      rewrite > H3.
1653      apply le_
1654     ]
1655   ]
1656 qed.
1657 *)
1658
1659 theorem le_A_exp4: \forall n. S O < n \to
1660 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1661 intro.
1662 apply (nat_elim1 n).
1663 intros.
1664 elim (or_eq_eq_S m).
1665 elim H2
1666   [elim (le_to_or_lt_eq (S O) a)
1667     [rewrite > H3 in ⊢ (? % ?).
1668      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1669       [apply le_A_exp
1670       |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1671         [apply le_times_r.
1672          apply H
1673           [rewrite > H3.
1674            rewrite > times_n_SO in ⊢ (? % ?).
1675            rewrite > sym_times.
1676            apply lt_times_l1
1677             [apply lt_to_le.assumption
1678             |apply le_n
1679             ]
1680           |assumption
1681           ]
1682         |rewrite < H3.
1683          rewrite < assoc_times.
1684          rewrite > sym_times in ⊢ (? (? % ?) ?).
1685          rewrite > assoc_times.
1686          apply le_times
1687           [rewrite > H3.
1688            elim a[apply le_n|simplify.apply le_plus_n_r]
1689           |rewrite < exp_plus_times.
1690            apply le_exp
1691             [apply lt_O_S
1692             |apply (trans_le ? (m+(m-3)))
1693               [apply le_plus_l.
1694                cases m[apply le_n|apply le_n_Sn]
1695               |simplify.rewrite < plus_n_O.
1696                rewrite > eq_minus_plus_plus_minus
1697                 [apply le_n
1698                 |rewrite > H3.
1699                  apply (trans_le ? (2*2))
1700                   [simplify.apply (le_n_Sn 3)
1701                   |apply le_times_r.assumption
1702                   ]
1703                 ]
1704               ]
1705             ]
1706           ]
1707         ]
1708       ]
1709     |rewrite > H3.rewrite < H4.simplify.
1710      apply le_S_S.apply lt_O_S
1711     |apply not_lt_to_le.intro.
1712      apply (lt_to_not_le ? ? H1).
1713      rewrite > H3.
1714      apply (le_n_O_elim a)
1715       [apply le_S_S_to_le.assumption
1716       |apply le_O_n
1717       ]
1718     ]
1719   |elim (le_to_or_lt_eq O a (le_O_n ?))
1720     [apply (trans_le ? (A ((S(S O))*(S a))))
1721       [apply monotonic_A.
1722        rewrite > H3.
1723        rewrite > times_SSO.
1724        apply le_n_Sn
1725       |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1726         [apply le_A_exp
1727         |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1728           [apply le_times_r.
1729            apply H
1730             [rewrite > H3.
1731              apply le_S_S.
1732              apply le_S_times_SSO.
1733              assumption
1734             |apply le_S_S.assumption
1735             ]
1736           |rewrite > H3.
1737            change in ⊢ (? ? (? % ?)) with (2*a).
1738            rewrite > times_SSO.
1739            change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1740            rewrite > minus_Sn_m
1741             [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1742              rewrite < assoc_times in ⊢ (? (? ? %) ?).
1743              rewrite < assoc_times.
1744              rewrite > sym_times in ⊢ (? (? % ?) ?).
1745              rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1746              rewrite > assoc_times.
1747              apply le_times_r.
1748              rewrite < exp_plus_times.
1749              apply le_exp
1750               [apply lt_O_S
1751               |rewrite < eq_minus_plus_plus_minus
1752                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1753                  apply le_n
1754                 |apply le_S_S.
1755                  apply O_lt_const_to_le_times_const.
1756                  assumption
1757                 ]
1758               ]
1759             |apply le_S_S.
1760              apply O_lt_const_to_le_times_const.
1761              assumption
1762             ]
1763           ]
1764         ]
1765       ]
1766     |rewrite < H4 in H3.simplify in H3.
1767      apply False_ind.
1768      apply (lt_to_not_le ? ? H1).
1769      rewrite > H3.
1770      apply le_n
1771     ]
1772   ]
1773 qed.
1774
1775 theorem le_n_SSSSSSSSO_to_le_A_exp:
1776 \forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
1777 intro.cases n
1778   [intro.apply le_n
1779   |cases n1
1780     [intro.apply le_n
1781     |cases n2
1782       [intro.apply le_n
1783       |cases n3
1784         [intro.apply leb_true_to_le.reflexivity
1785         |cases n4
1786           [intro.apply leb_true_to_le.reflexivity
1787           |cases n5
1788             [intro.apply leb_true_to_le.reflexivity
1789             |cases n6
1790               [intro.apply leb_true_to_le.reflexivity
1791               |cases n7
1792                 [intro.apply leb_true_to_le.reflexivity
1793                 |cases n8
1794                   [intro.apply leb_true_to_le.reflexivity
1795                   |intro.apply False_ind.
1796                    apply (lt_to_not_le ? ? H).
1797                    apply leb_true_to_le.reflexivity
1798                   ]
1799                 ]
1800               ]
1801             ]
1802           ]
1803         ]
1804       ]
1805     ]
1806   ]
1807 qed.
1808
1809 theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
1810 intro.
1811 apply (nat_elim1 n).
1812 intros.
1813 elim (decidable_le 9 m)
1814   [elim (or_eq_eq_S m).
1815    elim H2
1816     [rewrite > H3 in ⊢ (? % ?).
1817      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1818       [apply le_A_exp
1819       |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
1820         [apply le_times_r.
1821          apply H.
1822          rewrite > H3.
1823          apply lt_m_nm
1824           [apply (trans_lt ? 4)
1825             [apply lt_O_S
1826             |apply (lt_times_to_lt 2)
1827               [apply lt_O_S
1828               |rewrite < H3.assumption
1829               ]
1830             ]
1831           |apply le_n
1832           ]
1833         |rewrite < H3.
1834          rewrite < exp_plus_times.
1835          apply le_exp
1836           [apply lt_O_S
1837           |simplify.rewrite < plus_n_O.
1838            rewrite > eq_minus_plus_plus_minus
1839             [apply le_plus_l.
1840              apply le_pred_n
1841             |apply (trans_le ? 9)
1842               [apply leb_true_to_le. reflexivity
1843               |assumption
1844               ]
1845             ]
1846           ]
1847         ]
1848       ]
1849     |apply (trans_le ? (A (2*(S a))))
1850       [apply monotonic_A.
1851        rewrite > H3.
1852        rewrite > times_SSO.
1853        apply le_n_Sn
1854       |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
1855         [apply lt_SSSSO_to_le_A_exp.
1856          apply le_S_S.
1857          apply (le_times_to_le 2)
1858           [apply le_n_Sn.
1859           |apply le_S_S_to_le.rewrite < H3.assumption
1860           ]
1861         |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
1862           [apply le_times_r.
1863            apply H.
1864            rewrite > H3.
1865            apply le_S_S.
1866            apply lt_m_nm
1867             [apply (lt_to_le_to_lt ? 4)
1868               [apply lt_O_S
1869               |apply (le_times_to_le 2)
1870                 [apply lt_O_S
1871                 |apply le_S_S_to_le.
1872                  rewrite < H3.assumption
1873                 ]
1874               ]
1875             |apply le_n
1876             ]
1877           |rewrite > times_SSO.
1878            rewrite < H3.
1879            rewrite < exp_plus_times.
1880            apply le_exp
1881             [apply lt_O_S
1882             |cases m
1883               [apply le_n
1884               |cases n1
1885                 [apply le_n
1886                 |simplify.
1887                  rewrite < minus_n_O.
1888                  rewrite < plus_n_O.
1889                  rewrite < plus_n_Sm.
1890                  simplify.rewrite < minus_n_O.
1891                  rewrite < plus_n_Sm.
1892                  apply le_n
1893                 ]
1894               ]
1895             ]
1896           ]
1897         ]
1898       ]
1899     ]
1900   |apply le_n_SSSSSSSSO_to_le_A_exp.
1901    apply le_S_S_to_le.
1902    apply not_le_to_lt.
1903    assumption
1904   ]
1905 qed.
1906
1907 theorem eq_sigma_pi_SO_n: \forall n.
1908 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1909 intro.elim n
1910   [reflexivity
1911   |rewrite > true_to_sigma_p_Sn
1912     [rewrite > H.reflexivity
1913     |reflexivity
1914     ]
1915   ]
1916 qed.
1917
1918 theorem leA_prim: \forall n.
1919 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1920 intro.
1921 unfold prim.
1922 rewrite < (exp_sigma_p (S n) n primeb).
1923 unfold A.
1924 rewrite < times_pi_p.
1925 apply le_pi_p.
1926 intros.
1927 rewrite > sym_times.
1928 change in ⊢ (? ? %) with (exp i (S (log i n))).
1929 apply lt_to_le.
1930 apply lt_exp_log.
1931 apply prime_to_lt_SO.
1932 apply primeb_true_to_prime.
1933 assumption.
1934 qed.
1935
1936
1937 theorem le_prim_log : \forall n,b.S O < b \to
1938 log b (A n) \leq prim n * (S (log b n)).
1939 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
1940   [apply le_log
1941      [assumption
1942      |apply le_Al]
1943   |assumption]
1944 qed.
1945
1946
1947 (* the inequalities *)
1948 theorem le_exp_priml: \forall n. O < n \to
1949 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1950 intros.
1951 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1952   [apply le_exp_B.assumption
1953   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1954    apply le_times_r.
1955    apply (trans_le ? (A ((S(S O))*n)))
1956     [apply le_B_A
1957     |apply le_Al
1958     ]
1959   ]
1960 qed.
1961
1962 theorem le_exp_prim4l: \forall n. O < n \to
1963 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
1964 intros.
1965 apply (trans_le ? (2*(4*n*(B (4*n)))))
1966   [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
1967    apply le_times_r.
1968    cut (4*n = 2*(2*n))
1969     [rewrite > Hcut.
1970      apply le_exp_B.
1971      apply lt_to_le.unfold.
1972      rewrite > times_n_SO in ⊢ (? % ?).
1973      apply le_times_r.assumption
1974     |rewrite < assoc_times.
1975      reflexivity
1976     ]
1977   |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
1978    rewrite < assoc_times.
1979    rewrite > sym_times in ⊢ (? (? % ?) ?).
1980    rewrite > assoc_times.
1981    apply le_times_r.
1982    apply (trans_le ? (A (4*n)))
1983     [apply le_B_A4.assumption
1984     |apply le_Al
1985     ]
1986   ]
1987 qed.
1988
1989 theorem le_priml: \forall n. O < n \to
1990 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1991 intros.
1992 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1993   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1994     [apply le_log
1995       [apply le_n
1996       |apply le_exp_priml.assumption
1997       ]
1998     |rewrite > sym_times in ⊢ (? ? %).
1999      apply log_exp1.
2000      apply le_n
2001     ]
2002   |apply le_n
2003   ]
2004 qed.
2005
2006 theorem le_exp_primr: \forall n.
2007 exp n (prim n) \le exp 2 (2*(2*n-3)).
2008 intros.
2009 apply (trans_le ? (exp (A n) 2))
2010   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
2011    rewrite < times_n_SO.
2012    apply leA_r2
2013   |rewrite > sym_times.
2014    rewrite < exp_exp_times.
2015    apply monotonic_exp1.
2016    apply le_A_exp5
2017   ]
2018 qed.
2019