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