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

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/log.ma".
  16 include "nat/pi_p.ma".
  17 include "nat/factorization.ma".
  18 include "nat/factorial2.ma".
  19
  20 definition prim: nat \to nat \def
  21 \lambda n. sigma_p (S n) primeb (\lambda p.1).
  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 (* la prova potrebbe essere migliorata *)
 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 1 < 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.1).
 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) (λm:nat.leb (S O) m)
 801    (λm.pi_p (S m) primeb
 802     (\lambda p.(pi_p (log p m)
 803      (\lambda i.divides_b (exp p (S i)) m) (\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) (λm:nat.leb (S O) m)
 811      (λm:nat
 812       .pi_p (S m) (\lambda p.primeb p\land leb p m)
 813        (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λ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) (λm:nat.leb (S O) m)
 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 (2*n) =
1013 pi_p (S (2*n)) primeb
1014   (\lambda p.(pi_p (log p (2*n))
1015     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))))).
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 (2*n) =
1035 pi_p (S (2*n)) primeb
1036   (\lambda p.(pi_p (log p (2*n))
1037     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))*
1038 pi_p (S (2*n)) primeb
1039   (\lambda p.(pi_p (log p (2*n))
1040     (\lambda i.true) (\lambda i.(exp p (mod (2*n /(exp p (S i))) 2))))).
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. 1 < n \to
1051 pi_p (S (2*n)) primeb
1052   (\lambda p.(pi_p (log p (2*n))
1053     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
1054 =
1055 pi_p (S n) primeb
1056   (\lambda p.(pi_p (log p (2*n))
1057     (\lambda i.true) (\lambda i.(exp p (2*(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. 1 < n \to
1080 pi_p (S (2*n)) primeb
1081   (\lambda p.(pi_p (log p ((S(S O))*n))
1082     (\lambda i.true) (\lambda i.(exp p (2*(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 (2*(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) 2
1122 =
1123 pi_p (S n) primeb
1124   (\lambda p.(pi_p (log p n)
1125     (\lambda i.true) (\lambda i.(exp p (2*(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 (2*n) = exp (fact n) 2 * B(2*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 (* not usefull
1280 theorem le_fact_A:\forall n.S O < n \to
1281 fact (2*n) \le exp (fact n) 2 * A (2*n).
1282 intros.
1283 rewrite > eq_fact_B
1284   [apply le_times_r.
1285    apply le_B_A
1286   |assumption
1287   ]
1288 qed. *)
1289
1290 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1291 B (2*n) \le exp 2 (pred (2*n)).
1292 intros.
1293 apply (le_times_to_le (exp (fact n) (S(S O))))
1294   [apply lt_O_exp.
1295    apply lt_O_fact
1296   |rewrite < eq_fact_B
1297     [rewrite < sym_times in ⊢ (? ? %).
1298      rewrite > exp_SSO.
1299      rewrite < assoc_times.
1300      apply fact1
1301     |assumption
1302     ]
1303   ]
1304 qed.
1305
1306 theorem le_B_exp: \forall n.
1307 B (2*n) \le exp 2 (pred (2*n)).
1308 intro.cases n
1309   [apply le_n
1310   |cases n1
1311     [simplify.apply le_n
1312     |apply lt_SO_to_le_B_exp.
1313      apply le_S_S.apply lt_O_S.
1314     ]
1315   ]
1316 qed.
1317
1318 theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
1319 B (2*n) \le exp 2 ((2*n)-2).
1320 intros.
1321 apply (le_times_to_le (exp (fact n) (S(S O))))
1322   [apply lt_O_exp.
1323    apply lt_O_fact
1324   |rewrite < eq_fact_B
1325     [rewrite < sym_times in ⊢ (? ? %).
1326      rewrite > exp_SSO.
1327      rewrite < assoc_times.
1328      apply lt_SSSSO_to_fact.assumption
1329     |apply lt_to_le.apply lt_to_le.
1330      apply lt_to_le.assumption
1331     ]
1332   ]
1333 qed.
1334
1335 theorem lt_SO_to_le_exp_B: \forall n. 1 < n \to
1336 exp 2 (2*n) \le 2 * n * B (2*n).
1337 intros.
1338 apply (le_times_to_le (exp (fact n) (S(S O))))
1339   [apply lt_O_exp.
1340    apply lt_O_fact
1341   |rewrite < assoc_times in ⊢ (? ? %).
1342    rewrite > sym_times in ⊢ (? ? (? % ?)).
1343    rewrite > assoc_times in ⊢ (? ? %).
1344    rewrite < eq_fact_B
1345     [rewrite < sym_times.
1346      apply fact3.
1347      apply lt_to_le.assumption
1348     |assumption
1349     ]
1350   ]
1351 qed.
1352
1353 theorem le_exp_B: \forall n. O < n \to
1354 exp 2 (2*n) \le 2 * n * B (2*n).
1355 intros.
1356 elim H
1357   [apply le_n
1358   |apply lt_SO_to_le_exp_B.
1359    apply le_S_S.assumption
1360   ]
1361 qed.
1362
1363 theorem eq_A_SSO_n: \forall n.O < n \to
1364 A(2*n) =
1365  pi_p (S (2*n)) primeb
1366   (\lambda p.(pi_p (log p (2*n) )
1367     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1368  *A n.
1369 intro.
1370 rewrite > eq_A_A'.rewrite > eq_A_A'.
1371 unfold A'.intros.
1372 cut (
1373  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1374  = pi_p (S ((S(S O))*n)) primeb
1375     (λ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))))))))
1376   [rewrite > Hcut.
1377    rewrite < times_pi_p.
1378    apply eq_pi_p1;intros
1379     [reflexivity
1380     |rewrite < times_pi_p.
1381      apply eq_pi_p;intros
1382       [reflexivity
1383       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1384         [simplify.rewrite < times_n_SO.apply times_n_SO
1385         |simplify.rewrite < plus_n_O.apply times_n_SO
1386         ]
1387       ]
1388     ]
1389   |apply (trans_eq ? ? (pi_p (S n) primeb
1390     (\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))))))))
1391     [apply eq_pi_p1;intros
1392       [reflexivity
1393       |apply eq_pi_p1;intros
1394         [reflexivity
1395         |rewrite > lt_to_leb_false
1396           [simplify.apply times_n_SO
1397           |apply le_S_S.
1398            apply (trans_le ? (exp x (log x n)))
1399             [apply le_exp
1400               [apply prime_to_lt_O.
1401                apply primeb_true_to_prime.
1402                assumption
1403               |assumption
1404               ]
1405             |apply le_exp_log.
1406              assumption
1407             ]
1408           ]
1409         ]
1410       ]
1411     |apply (trans_eq ? ?
1412       (pi_p (S ((S(S O))*n)) primeb
1413        (λp:nat.pi_p (log p n) (λi:nat.true)
1414         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1415       [apply sym_eq.
1416        apply or_false_eq_SO_to_eq_pi_p
1417         [apply le_S_S.
1418          simplify.
1419          apply le_plus_n_r
1420         |intros.right.
1421          rewrite > lt_to_log_O
1422           [reflexivity
1423           |assumption
1424           |assumption
1425           ]
1426         ]
1427       |apply eq_pi_p1;intros
1428         [reflexivity
1429         |apply sym_eq.
1430          apply or_false_eq_SO_to_eq_pi_p
1431           [apply le_log
1432             [apply prime_to_lt_SO.
1433              apply primeb_true_to_prime.
1434              assumption
1435             |simplify.
1436              apply le_plus_n_r
1437             ]
1438           |intros.right.
1439            rewrite > le_to_leb_true
1440             [simplify.reflexivity
1441             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1442               [apply lt_exp_log.
1443                apply prime_to_lt_SO.
1444                apply primeb_true_to_prime.
1445                assumption
1446               |apply le_exp
1447                 [apply prime_to_lt_O.
1448                  apply primeb_true_to_prime.
1449                  assumption
1450                 |apply le_S_S.assumption
1451                 ]
1452               ]
1453             ]
1454           ]
1455         ]
1456       ]
1457     ]
1458   ]
1459 qed.
1460
1461 theorem le_A_BA1: \forall n. O < n \to
1462 A(2*n) \le B(2*n)*A n.
1463 intros.
1464 rewrite > eq_A_SSO_n
1465   [apply le_times_l.
1466    unfold B.
1467    apply le_pi_p.intros.
1468    apply le_pi_p.intros.
1469    apply le_exp
1470     [apply prime_to_lt_O.
1471      apply primeb_true_to_prime.
1472      assumption
1473     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1474       [simplify in ⊢ (? % ?).
1475        cut ((S(S O))*n/i\sup(S i1) = S O)
1476         [rewrite > Hcut.apply le_n
1477         |apply (div_mod_spec_to_eq
1478           ((S(S O))*n) (exp i (S i1))
1479            ? (mod ((S(S O))*n) (exp i (S i1)))
1480            ? (minus ((S(S O))*n) (exp i (S i1))) )
1481           [apply div_mod_spec_div_mod.
1482            apply lt_O_exp.
1483            apply prime_to_lt_O.
1484            apply primeb_true_to_prime.
1485            assumption
1486           |cut (i\sup(S i1)≤(S(S O))*n)
1487             [apply div_mod_spec_intro
1488               [apply lt_plus_to_lt_minus
1489                 [assumption
1490                 |simplify in ⊢ (? % ?).
1491                  rewrite < plus_n_O.
1492                  apply lt_plus
1493                   [apply leb_true_to_le.assumption
1494                   |apply leb_true_to_le.assumption
1495                   ]
1496                 ]
1497               |rewrite > sym_plus.
1498                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1499                rewrite < times_n_SO.
1500                apply plus_minus_m_m.
1501                assumption
1502               ]
1503             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1504               [apply le_exp
1505                 [apply prime_to_lt_O.
1506                  apply primeb_true_to_prime.
1507                  assumption
1508                 |assumption
1509                 ]
1510               |apply le_exp_log.
1511                rewrite > (times_n_O O) in ⊢ (? % ?).
1512                apply lt_times
1513                 [apply lt_O_S
1514                 |assumption
1515                 ]
1516               ]
1517             ]
1518           ]
1519         ]
1520       |apply le_O_n
1521       ]
1522     ]
1523   |assumption
1524   ]
1525 qed.
1526
1527 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1528 intros.cases n
1529   [apply le_n
1530   |apply le_A_BA1.apply lt_O_S
1531   ]
1532 qed.
1533
1534 theorem le_A_exp: \forall n.
1535 A(2*n) \le (exp 2 (pred (2*n)))*A n.
1536 intro.
1537 apply (trans_le ? (B(2*n)*A n))
1538   [apply le_A_BA
1539   |apply le_times_l.
1540    apply le_B_exp
1541   ]
1542 qed.
1543
1544 theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
1545 A(2*n) \le exp 2 ((2*n)-2)*A n.
1546 intros.
1547 apply (trans_le ? (B(2*n)*A n))
1548   [apply le_A_BA
1549   |apply le_times_l.
1550    apply lt_SSSSO_to_le_B_exp.assumption
1551   ]
1552 qed.
1553
1554 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1555 intro.cases n
1556   [apply le_n
1557   |simplify.apply le_plus_r.
1558    apply le_n_Sn
1559   ]
1560 qed.
1561
1562 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1563 intros.
1564 elim H
1565   [apply le_n
1566   |rewrite > times_SSO.
1567    apply le_S_S.
1568    apply (trans_le ? (2*n1))
1569     [assumption
1570     |apply le_n_Sn
1571     ]
1572   ]
1573 qed.
1574
1575 theorem le_A_exp1: \forall n.
1576 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1577 intro.elim n
1578   [simplify.apply le_n
1579   |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1580    apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1581     [apply le_A_exp
1582     |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1583       [apply le_times_r.
1584        assumption
1585       |rewrite < exp_plus_times.
1586        apply le_exp
1587         [apply lt_O_S
1588         |cut (S(S n1) \le 2*(exp 2 n1))
1589           [apply le_S_S_to_le.
1590            change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1591            rewrite < S_pred
1592             [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1593              rewrite < S_pred
1594               [rewrite < eq_minus_plus_plus_minus
1595                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1596                  apply le_n
1597                 |assumption
1598                 ]
1599               |apply lt_to_lt_O_minus.
1600                apply (lt_to_le_to_lt ? (2*(S(S n1))))
1601                 [rewrite > times_n_SO in ⊢ (? % ?).
1602                  rewrite > sym_times.
1603                  apply lt_times_l1
1604                   [apply lt_O_S
1605                   |apply le_n
1606                   ]
1607                 |apply le_times_r.
1608                  assumption
1609                 ]
1610               ]
1611             |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1612              apply le_times
1613               [apply le_n_Sn
1614               |apply lt_O_exp.
1615                apply lt_O_S
1616               ]
1617             ]
1618           |elim n1
1619             [apply le_n
1620             |apply (trans_le ? (2*(S(S n2))))
1621               [apply le_S_times_SSO.
1622                apply lt_O_S
1623               |apply le_times_r.
1624                assumption
1625               ]
1626             ]
1627           ]
1628         ]
1629       ]
1630     ]
1631   ]
1632 qed.
1633
1634 theorem monotonic_A: monotonic nat le A.
1635 unfold.intros.
1636 elim H
1637   [apply le_n
1638   |apply (trans_le ? (A n1))
1639     [assumption
1640     |unfold A.
1641      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1642           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1643       [apply (bool_elim ? (primeb (S n1)));intro
1644         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1645          rewrite > times_n_SO in ⊢ (? % ?).
1646          rewrite > sym_times.
1647          apply le_times
1648           [apply lt_O_exp.apply lt_O_S
1649           |assumption
1650           ]
1651         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1652          assumption
1653         ]
1654       |apply le_pi_p.intros.
1655        apply le_exp
1656         [apply prime_to_lt_O.
1657          apply primeb_true_to_prime.
1658          assumption
1659         |apply le_log
1660           [apply prime_to_lt_SO.
1661            apply primeb_true_to_prime.
1662            assumption
1663           |apply le_S.apply le_n
1664           ]
1665         ]
1666       ]
1667     ]
1668   ]
1669 qed.
1670
1671 (*
1672 theorem le_A_exp2: \forall n. O < n \to
1673 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1674 intros.
1675 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1676   [apply monotonic_A.
1677    apply lt_to_le.
1678    apply lt_exp_log.
1679    apply le_n
1680   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1681     [apply le_A_exp1
1682     |apply le_exp
1683       [apply lt_O_S
1684       |rewrite > assoc_times.apply le_times_r.
1685        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1686        apply le_times_r.
1687        apply le_exp_log.
1688        assumption
1689       ]
1690     ]
1691   ]
1692 qed.
1693 *)
1694
1695 (* example *)
1696 theorem A_SO: A (S O) = S O.
1697 reflexivity.
1698 qed.
1699
1700 theorem A_SSO: A (S(S O)) = S (S O).
1701 reflexivity.
1702 qed.
1703
1704 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1705 reflexivity.
1706 qed.
1707
1708 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1709 reflexivity.
1710 qed.
1711
1712 (*
1713 (* a better result *)
1714 theorem le_A_exp3: \forall n. S O < n \to
1715 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1716 intro.
1717 apply (nat_elim1 n).
1718 intros.
1719 elim (or_eq_eq_S m).
1720 elim H2
1721   [elim (le_to_or_lt_eq (S O) a)
1722     [rewrite > H3 in ⊢ (? % ?).
1723      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1724       [apply le_A_exp
1725       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1726          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1727         [apply le_times_r.
1728          apply H
1729           [rewrite > H3.
1730            rewrite > times_n_SO in ⊢ (? % ?).
1731            rewrite > sym_times.
1732            apply lt_times_l1
1733             [apply lt_to_le.assumption
1734             |apply le_n
1735             ]
1736           |assumption
1737           ]
1738         |rewrite > sym_times.
1739          rewrite > assoc_times.
1740          rewrite < exp_plus_times.
1741          apply (trans_le ?
1742           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1743           [rewrite > assoc_times.
1744            apply le_times_r.
1745            rewrite < exp_plus_times.
1746            apply le_exp
1747             [apply lt_O_S
1748             |rewrite < H3.
1749              simplify.
1750              rewrite < plus_n_O.
1751              apply le_S.apply le_S.
1752              apply le_n
1753             ]
1754           |apply le_times_l.
1755            rewrite > times_exp.
1756            apply monotonic_exp1.
1757            rewrite > H3.
1758            rewrite > sym_times.
1759            cases a
1760             [apply le_n
1761             |simplify.
1762              rewrite < plus_n_Sm.
1763              apply le_S.
1764              apply le_n
1765             ]
1766           ]
1767         ]
1768       ]
1769     |rewrite < H4 in H3.
1770      simplify in H3.
1771      rewrite > H3.
1772      simplify.
1773      apply le_S_S.apply le_S_S.apply le_O_n
1774     |apply not_lt_to_le.intro.
1775      apply (lt_to_not_le ? ? H1).
1776      rewrite > H3.
1777      apply (le_n_O_elim a)
1778       [apply le_S_S_to_le.assumption
1779       |apply le_O_n
1780       ]
1781     ]
1782   |elim (le_to_or_lt_eq O a (le_O_n ?))
1783     [apply (trans_le ? (A ((S(S O))*(S a))))
1784       [apply monotonic_A.
1785        rewrite > H3.
1786        rewrite > times_SSO.
1787        apply le_n_Sn
1788       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1789         [apply le_A_exp
1790         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1791            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1792           [apply le_times_r.
1793            apply H
1794             [rewrite > H3.
1795              apply le_S_S.
1796              simplify.
1797              rewrite > plus_n_SO.
1798              apply le_plus_r.
1799              rewrite < plus_n_O.
1800              assumption
1801             |apply le_S_S.assumption
1802             ]
1803           |rewrite > sym_times.
1804            rewrite > assoc_times.
1805            rewrite < exp_plus_times.
1806            apply (trans_le ?
1807             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1808             [rewrite > assoc_times.
1809              apply le_times_r.
1810              rewrite < exp_plus_times.
1811              apply le_exp
1812               [apply lt_O_S
1813               |rewrite > times_SSO.
1814                rewrite < H3.
1815                simplify.
1816                rewrite < plus_n_Sm.
1817                rewrite < plus_n_O.
1818                apply le_n
1819               ]
1820             |apply le_times_l.
1821              rewrite > times_exp.
1822              apply monotonic_exp1.
1823              rewrite > H3.
1824              rewrite > sym_times.
1825              apply le_n
1826             ]
1827           ]
1828         ]
1829       ]
1830     |rewrite < H4 in H3.simplify in H3.
1831      apply False_ind.
1832      apply (lt_to_not_le ? ? H1).
1833      rewrite > H3.
1834      apply le_
1835     ]
1836   ]
1837 qed.
1838 *)
1839
1840 theorem le_A_exp4: \forall n. S O < n \to
1841 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1842 intro.
1843 apply (nat_elim1 n).
1844 intros.
1845 elim (or_eq_eq_S m).
1846 elim H2
1847   [elim (le_to_or_lt_eq (S O) a)
1848     [rewrite > H3 in ⊢ (? % ?).
1849      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1850       [apply le_A_exp
1851       |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1852         [apply le_times_r.
1853          apply H
1854           [rewrite > H3.
1855            rewrite > times_n_SO in ⊢ (? % ?).
1856            rewrite > sym_times.
1857            apply lt_times_l1
1858             [apply lt_to_le.assumption
1859             |apply le_n
1860             ]
1861           |assumption
1862           ]
1863         |rewrite < H3.
1864          rewrite < assoc_times.
1865          rewrite > sym_times in ⊢ (? (? % ?) ?).
1866          rewrite > assoc_times.
1867          apply le_times
1868           [rewrite > H3.
1869            elim a[apply le_n|simplify.apply le_plus_n_r]
1870           |rewrite < exp_plus_times.
1871            apply le_exp
1872             [apply lt_O_S
1873             |apply (trans_le ? (m+(m-3)))
1874               [apply le_plus_l.
1875                cases m[apply le_n|apply le_n_Sn]
1876               |simplify.rewrite < plus_n_O.
1877                rewrite > eq_minus_plus_plus_minus
1878                 [apply le_n
1879                 |rewrite > H3.
1880                  apply (trans_le ? (2*2))
1881                   [simplify.apply (le_n_Sn 3)
1882                   |apply le_times_r.assumption
1883                   ]
1884                 ]
1885               ]
1886             ]
1887           ]
1888         ]
1889       ]
1890     |rewrite > H3.rewrite < H4.simplify.
1891      apply le_S_S.apply lt_O_S
1892     |apply not_lt_to_le.intro.
1893      apply (lt_to_not_le ? ? H1).
1894      rewrite > H3.
1895      apply (le_n_O_elim a)
1896       [apply le_S_S_to_le.assumption
1897       |apply le_O_n
1898       ]
1899     ]
1900   |elim (le_to_or_lt_eq O a (le_O_n ?))
1901     [apply (trans_le ? (A ((S(S O))*(S a))))
1902       [apply monotonic_A.
1903        rewrite > H3.
1904        rewrite > times_SSO.
1905        apply le_n_Sn
1906       |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1907         [apply le_A_exp
1908         |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1909           [apply le_times_r.
1910            apply H
1911             [rewrite > H3.
1912              apply le_S_S.
1913              apply le_S_times_SSO.
1914              assumption
1915             |apply le_S_S.assumption
1916             ]
1917           |rewrite > H3.
1918            change in ⊢ (? ? (? % ?)) with (2*a).
1919            rewrite > times_SSO.
1920            change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1921            rewrite > minus_Sn_m
1922             [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1923              rewrite < assoc_times in ⊢ (? (? ? %) ?).
1924              rewrite < assoc_times.
1925              rewrite > sym_times in ⊢ (? (? % ?) ?).
1926              rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1927              rewrite > assoc_times.
1928              apply le_times_r.
1929              rewrite < exp_plus_times.
1930              apply le_exp
1931               [apply lt_O_S
1932               |rewrite < eq_minus_plus_plus_minus
1933                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1934                  apply le_n
1935                 |apply le_S_S.
1936                  apply O_lt_const_to_le_times_const.
1937                  assumption
1938                 ]
1939               ]
1940             |apply le_S_S.
1941              apply O_lt_const_to_le_times_const.
1942              assumption
1943             ]
1944           ]
1945         ]
1946       ]
1947     |rewrite < H4 in H3.simplify in H3.
1948      apply False_ind.
1949      apply (lt_to_not_le ? ? H1).
1950      rewrite > H3.
1951      apply le_n
1952     ]
1953   ]
1954 qed.
1955
1956 theorem le_n_SSSSSSSSO_to_le_A_exp:
1957 \forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
1958 intro.cases n
1959   [intro.apply le_n
1960   |cases n1
1961     [intro.apply le_n
1962     |cases n2
1963       [intro.apply le_n
1964       |cases n3
1965         [intro.apply leb_true_to_le.reflexivity
1966         |cases n4
1967           [intro.apply leb_true_to_le.reflexivity
1968           |cases n5
1969             [intro.apply leb_true_to_le.reflexivity
1970             |cases n6
1971               [intro.apply leb_true_to_le.reflexivity
1972               |cases n7
1973                 [intro.apply leb_true_to_le.reflexivity
1974                 |cases n8
1975                   [intro.apply leb_true_to_le.reflexivity
1976                   |intro.apply False_ind.
1977                    apply (lt_to_not_le ? ? H).
1978                    apply leb_true_to_le.reflexivity
1979                   ]
1980                 ]
1981               ]
1982             ]
1983           ]
1984         ]
1985       ]
1986     ]
1987   ]
1988 qed.
1989
1990 theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
1991 intro.
1992 apply (nat_elim1 n).
1993 intros.
1994 elim (decidable_le 9 m)
1995   [elim (or_eq_eq_S m).
1996    elim H2
1997     [rewrite > H3 in ⊢ (? % ?).
1998      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1999       [apply le_A_exp
2000       |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
2001         [apply le_times_r.
2002          apply H.
2003          rewrite > H3.
2004          apply lt_m_nm
2005           [apply (trans_lt ? 4)
2006             [apply lt_O_S
2007             |apply (lt_times_to_lt 2)
2008               [apply lt_O_S
2009               |rewrite < H3.assumption
2010               ]
2011             ]
2012           |apply le_n
2013           ]
2014         |rewrite < H3.
2015          rewrite < exp_plus_times.
2016          apply le_exp
2017           [apply lt_O_S
2018           |simplify.rewrite < plus_n_O.
2019            rewrite > eq_minus_plus_plus_minus
2020             [apply le_plus_l.
2021              apply le_pred_n
2022             |apply (trans_le ? 9)
2023               [apply leb_true_to_le. reflexivity
2024               |assumption
2025               ]
2026             ]
2027           ]
2028         ]
2029       ]
2030     |apply (trans_le ? (A (2*(S a))))
2031       [apply monotonic_A.
2032        rewrite > H3.
2033        rewrite > times_SSO.
2034        apply le_n_Sn
2035       |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
2036         [apply lt_SSSSO_to_le_A_exp.
2037          apply le_S_S.
2038          apply (le_times_to_le 2)
2039           [apply le_n_Sn.
2040           |apply le_S_S_to_le.rewrite < H3.assumption
2041           ]
2042         |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
2043           [apply le_times_r.
2044            apply H.
2045            rewrite > H3.
2046            apply le_S_S.
2047            apply lt_m_nm
2048             [apply (lt_to_le_to_lt ? 4)
2049               [apply lt_O_S
2050               |apply (le_times_to_le 2)
2051                 [apply lt_O_S
2052                 |apply le_S_S_to_le.
2053                  rewrite < H3.assumption
2054                 ]
2055               ]
2056             |apply le_n
2057             ]
2058           |rewrite > times_SSO.
2059            rewrite < H3.
2060            rewrite < exp_plus_times.
2061            apply le_exp
2062             [apply lt_O_S
2063             |cases m
2064               [apply le_n
2065               |cases n1
2066                 [apply le_n
2067                 |simplify.
2068                  rewrite < minus_n_O.
2069                  rewrite < plus_n_O.
2070                  rewrite < plus_n_Sm.
2071                  simplify.rewrite < minus_n_O.
2072                  rewrite < plus_n_Sm.
2073                  apply le_n
2074                 ]
2075               ]
2076             ]
2077           ]
2078         ]
2079       ]
2080     ]
2081   |apply le_n_SSSSSSSSO_to_le_A_exp.
2082    apply le_S_S_to_le.
2083    apply not_le_to_lt.
2084    assumption
2085   ]
2086 qed.
2087
2088 theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n).
2089 intros.
2090 apply (trans_le ? ((exp 2 (2*n))/(2*n)))
2091   [apply le_times_to_le_div
2092     [rewrite > (times_n_O O) in ⊢ (? % ?).
2093      apply lt_times
2094       [apply lt_O_S
2095       |assumption
2096       ]
2097     |simplify in ⊢ (? ? (? ? %)).
2098      rewrite < plus_n_O.
2099      rewrite > exp_plus_times.
2100      apply le_times_l.
2101      alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con".
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