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