helm/software/matita/library/nat/bertrand.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/sqrt.ma".
  16 include "nat/chebyshev_teta.ma".
  17 include "nat/chebyshev.ma".
  18 include "nat/o.ma".
  19
  20 definition bertrand \def \lambda n.
  21 \exists p.n < p \land p \le 2*n \land (prime p).
  22
  23 definition not_bertrand \def \lambda n.
  24 \forall p.n < p \to p \le 2*n \to \not (prime p).
  25
  26 lemma not_not_bertrand_to_bertrand1: \forall n.
  27 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
  28 (\forall p.x < p \to p \le 2*n \to \not (prime p))
  29 \to \exists p.n < p \land p \le  x \land (prime p).
  30 intros 4.elim H1
  31   [apply False_ind.apply H.assumption
  32   |apply (bool_elim ? (primeb (S n1)));intro
  33     [apply (ex_intro ? ? (S n1)).
  34      split
  35       [split
  36         [apply le_S_S.assumption
  37         |apply le_n
  38         ]
  39       |apply primeb_true_to_prime.assumption
  40       ]
  41     |elim H3
  42       [elim H7.clear H7.
  43        elim H8.clear H8.
  44        apply (ex_intro ? ? a).
  45        split
  46         [split
  47           [assumption
  48           |apply le_S.assumption
  49           ]
  50         |assumption
  51         ]
  52       |apply lt_to_le.assumption
  53       |elim (le_to_or_lt_eq ? ? H7)
  54         [apply H5;assumption
  55         |rewrite < H9.
  56          apply primeb_false_to_not_prime.
  57          assumption
  58         ]
  59       ]
  60     ]
  61   ]
  62 qed.
  63
  64 theorem not_not_bertrand_to_bertrand: \forall n.
  65 \lnot (not_bertrand n) \to bertrand n.
  66 unfold bertrand.intros.
  67 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
  68   [assumption
  69   |apply le_times_n.apply le_n_Sn
  70   |apply le_n
  71   |intros.apply False_ind.
  72    apply (lt_to_not_le ? ? H1 H2)
  73   ]
  74 qed.
  75
  76 (* not used
  77 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
  78 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
  79 divides p (g i))).
  80 intros 2.elim n
  81   [simplify in H1.
  82    apply False_ind.
  83    apply (le_to_not_lt p 1)
  84     [apply divides_to_le
  85       [apply le_n
  86       |assumption
  87       ]
  88     |elim H.assumption
  89     ]
  90   |apply (bool_elim ? (b n1));intro
  91     [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
  92      elim (divides_times_to_divides ? ? ? H1 H2)
  93       [apply (ex_intro ? ? n1).
  94        split
  95         [apply le_n
  96         |split;assumption
  97         ]
  98       |elim (H ? ? H1 H4).
  99        elim H5.
 100        apply (ex_intro ? ? a).
 101        split
 102         [apply lt_to_le.apply le_S_S.assumption
 103         |assumption
 104         ]
 105       ]
 106     |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
 107      elim (H ? ? H1 H2).
 108      elim H4.
 109      apply (ex_intro ? ? a).
 110      split
 111       [apply lt_to_le.apply le_S_S.assumption
 112       |assumption
 113       ]
 114     ]
 115   ]
 116 qed.
 117
 118 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
 119 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
 120 intros.
 121 unfold B in H1.
 122 elim (divides_pi_p_to_divides ? ? ? ? H H1).
 123 elim H2.clear H2.
 124 elim H4.clear H4.
 125 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
 126 elim H4.clear H4.
 127 elim H6.clear H6.
 128 cut (p = a)
 129   [split
 130     [rewrite > Hcut.apply le_S_S_to_le.assumption
 131     |apply (ex_intro ? ? a1).
 132      rewrite > Hcut.
 133      intro.
 134      change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
 135      rewrite > H6 in H7.
 136      simplify in H7.
 137      absurd (p \le 1)
 138       [apply divides_to_le[apply lt_O_S|assumption]
 139       |apply lt_to_not_le.elim H.assumption
 140       ]
 141     ]
 142   |apply (divides_exp_to_eq ? ? ? H ? H7).
 143    apply primeb_true_to_prime.
 144    assumption
 145   ]
 146 qed.
 147 *)
 148
 149 definition k \def \lambda n,p.
 150 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
 151
 152 theorem le_k: \forall n,p. k n p \le log p n.
 153 intros.unfold k.elim (log p n)
 154   [apply le_n
 155   |rewrite > true_to_sigma_p_Sn
 156     [rewrite > plus_n_SO.
 157      rewrite > sym_plus in ⊢ (? ? %).
 158      apply le_plus
 159       [apply le_S_S_to_le.
 160        apply lt_mod_m_m.
 161        apply lt_O_S
 162       |assumption
 163       ]
 164     |reflexivity
 165     ]
 166   ]
 167 qed.
 168
 169 definition B1 \def
 170 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
 171
 172 theorem eq_B_B1: \forall n. B n = B1 n.
 173 intros.unfold B.unfold B1.
 174 apply eq_pi_p
 175   [intros.reflexivity
 176   |intros.unfold k.
 177    apply exp_sigma_p1
 178   ]
 179 qed.
 180
 181 definition B_split1 \def \lambda n.
 182 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
 183
 184 definition B_split2 \def \lambda n.
 185 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
 186
 187 theorem eq_B1_times_B_split1_B_split2: \forall n.
 188 B1 n = B_split1 n * B_split2 n.
 189 intro.unfold B1.unfold B_split1.unfold B_split2.
 190 rewrite < times_pi_p.
 191 apply eq_pi_p
 192   [intros.reflexivity
 193   |intros.apply (bool_elim ? (leb (k n x) 1));intro
 194     [rewrite > (lt_to_leb_false 2 (k n x))
 195       [simplify.rewrite < plus_n_O.
 196        rewrite < times_n_SO.reflexivity
 197       |apply le_S_S.apply leb_true_to_le.assumption
 198       ]
 199     |rewrite > (le_to_leb_true 2 (k n x))
 200       [simplify.rewrite < plus_n_O.
 201        rewrite < plus_n_O.reflexivity
 202       |apply not_le_to_lt.apply leb_false_to_not_le.assumption
 203       ]
 204     ]
 205   ]
 206 qed.
 207
 208 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
 209 intros.
 210 cut (O < m) as H2
 211   [apply not_le_to_lt.
 212    intro.apply (lt_to_not_le ? ? H1).
 213    apply le_times_to_le_div;assumption
 214   |apply (ltn_to_ltO ? ? H1)
 215   ]
 216 qed.
 217
 218 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
 219 intros.
 220 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 221   [apply div_mod_spec_div_mod.
 222    apply (ltn_to_ltO ? ? H)
 223   |apply div_mod_spec_intro
 224     [assumption
 225     |reflexivity
 226     ]
 227   ]
 228 qed.
 229
 230 (* the value of n could be smaller *)
 231 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
 232 intros.unfold k.
 233 elim (log p (2*n))
 234   [reflexivity
 235   |rewrite > true_to_sigma_p_Sn
 236     [rewrite > H3.
 237      rewrite < plus_n_O.
 238      cases n1
 239       [rewrite < exp_n_SO.
 240        cut (2*n/p = 2) as H4
 241         [rewrite > H4.reflexivity
 242         |apply lt_to_le_times_to_lt_S_to_div
 243           [apply (ltn_to_ltO ? ? H2)
 244           |rewrite < sym_times.
 245            apply le_times_r.
 246            assumption
 247           |rewrite > sym_times in ⊢ (? ? %).
 248            apply lt_div_to_times
 249             [apply lt_O_S
 250             |assumption
 251             ]
 252           ]
 253         ]
 254       |cut (2*n/(p)\sup(S (S n2)) = O) as H4
 255         [rewrite > H4.reflexivity
 256         |apply lt_to_div_O.
 257          apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 258           [apply (le_times_to_le (exp 3 2))
 259             [apply leb_true_to_le.reflexivity
 260             |rewrite > sym_times in ⊢ (? ? %).
 261              rewrite > times_exp.
 262              apply (trans_le ? (exp n 2))
 263               [rewrite < assoc_times.
 264                rewrite > exp_SSO in ⊢ (? ? %).
 265                apply le_times_l.
 266                assumption
 267               |apply monotonic_exp1.
 268                apply (le_plus_to_le 3).
 269                change in ⊢ (? ? %) with ((S(2*n/3))*3).
 270                apply (trans_le ? (2*n))
 271                 [simplify in ⊢ (? ? %).
 272                  rewrite < plus_n_O.
 273                  apply le_plus_l.
 274                  apply (trans_le ? 18 ? ? H).
 275                  apply leb_true_to_le.reflexivity
 276                 |apply lt_to_le.
 277                  apply lt_div_S.
 278                  apply lt_O_S
 279                 ]
 280               ]
 281             ]
 282           |apply (lt_to_le_to_lt ? (exp p 2))
 283             [apply lt_exp1
 284               [apply lt_O_S
 285               |assumption
 286               ]
 287             |apply le_exp
 288               [apply (ltn_to_ltO ? ? H2)
 289               |apply le_S_S.apply le_S_S.apply le_O_n
 290               ]
 291             ]
 292           ]
 293         ]
 294       ]
 295     |reflexivity
 296     ]
 297   ]
 298 qed.
 299
 300 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 301 B_split1 (2*n) \le teta (2 * n / 3).
 302 intros.unfold B_split1.unfold teta.
 303 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 304   [apply le_pi_p.intros.
 305    apply le_exp
 306     [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
 307     |apply (bool_elim ? (leb (k (2*n) i) 1));intro
 308       [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
 309         [lapply (le_S_S_to_le ? ? H5) as H6.
 310          apply (le_n_O_elim ? H6).
 311          rewrite < times_n_O.
 312          apply le_n
 313         |rewrite > (eq_to_eqb_true ? ? H5).
 314          rewrite > H5.apply le_n
 315         ]
 316       |apply le_O_n
 317       ]
 318     ]
 319   |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 320     [apply (eq_ind ? ? ? (le_n ?)).
 321      apply or_false_eq_SO_to_eq_pi_p
 322       [apply le_S_S.
 323        apply le_times_to_le_div2
 324         [apply lt_O_S
 325         |rewrite > sym_times in ⊢ (? ? %).
 326          apply le_times_n.
 327          apply leb_true_to_le.reflexivity
 328         ]
 329       |intros.
 330        unfold not_bertrand in H1.
 331        elim (decidable_le (S n) i)
 332         [left.
 333          apply not_prime_to_primeb_false.
 334          apply H1
 335           [assumption
 336           |apply le_S_S_to_le.assumption
 337           ]
 338         |right.
 339          rewrite > k1
 340           [reflexivity
 341           |assumption
 342           |apply le_S_S_to_le.
 343            apply not_le_to_lt.assumption
 344           |assumption
 345           ]
 346         ]
 347       ]
 348     |apply le_pi_p.intros.
 349      elim (eqb (k (2*n) i) 1)
 350       [rewrite < exp_n_SO.apply le_n
 351       |simplify.apply prime_to_lt_O.
 352        apply primeb_true_to_prime.
 353        assumption
 354       ]
 355     ]
 356   ]
 357 qed.
 358
 359 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
 360 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
 361 intros.unfold B_split2.
 362 cut (O < n)
 363   [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
 364         (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
 365     [apply (eq_ind ? ? ? (le_n ?)).
 366      apply or_false_eq_SO_to_eq_pi_p
 367       [apply le_S_S.
 368        apply le_sqrt_n_n
 369       |intros.
 370        apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 371         [apply False_ind.
 372          apply (lt_to_not_le ? ? H1).unfold sqrt.
 373          apply f_m_to_le_max
 374           [apply le_S_S_to_le.assumption
 375           |apply le_to_leb_true.
 376            rewrite < exp_SSO.
 377            apply not_lt_to_le.intro.
 378            apply (le_to_not_lt 2 (log i (2*n)))
 379             [apply (trans_le ? (k (2*n) i))
 380               [apply leb_true_to_le.assumption
 381               |apply le_k
 382               ]
 383             |apply le_S_S.unfold log.apply f_false_to_le_max
 384               [apply (ex_intro ? ? O).split
 385                 [apply le_O_n
 386                 |apply le_to_leb_true.simplify.
 387                  apply (trans_le ? n)
 388                   [assumption.
 389                   |apply le_plus_n_r
 390                   ]
 391                 ]
 392               |intros.apply lt_to_leb_false.
 393                apply (lt_to_le_to_lt ? (exp i 2))
 394                 [assumption
 395                 |apply le_exp
 396                   [apply (ltn_to_ltO ? ? H1)
 397                   |assumption
 398                   ]
 399                 ]
 400               ]
 401             ]
 402           ]
 403         |right.reflexivity
 404         ]
 405       ]
 406     |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
 407       [apply le_pi_p.intros.
 408        apply (trans_le ? (exp i (log i (2*n))))
 409         [apply le_exp
 410           [apply prime_to_lt_O.
 411            apply primeb_true_to_prime.
 412            assumption
 413           |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 414             [simplify in ⊢ (? (? % ?) ?).
 415              rewrite > sym_times.
 416              rewrite < times_n_SO.
 417              apply le_k
 418             |apply le_O_n
 419             ]
 420           ]
 421         |apply le_exp_log.
 422          rewrite > (times_n_O O) in ⊢ (? % ?).
 423          apply lt_times
 424           [apply lt_O_S
 425           |assumption
 426           ]
 427         ]
 428       |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
 429         [unfold prim.
 430          apply (eq_ind ? ? ? (le_n ?)).
 431          apply exp_sigma_p
 432         |apply le_exp
 433           [rewrite > (times_n_O O) in ⊢ (? % ?).
 434            apply lt_times
 435             [apply lt_O_S
 436             |assumption
 437             ]
 438           |apply le_prim_n3.
 439            unfold sqrt.
 440            apply f_m_to_le_max
 441             [apply (trans_le ? (2*(exp 2 7)))
 442               [apply leb_true_to_le.reflexivity
 443               |apply le_times_r.assumption
 444               ]
 445             |apply le_to_leb_true.
 446              apply (trans_le ? (2*(exp 2 7)))
 447               [apply leb_true_to_le.reflexivity
 448               |apply le_times_r.assumption
 449               ]
 450             ]
 451           ]
 452         ]
 453       ]
 454     ]
 455   |apply (lt_to_le_to_lt ? ? ? ? H).
 456    apply leb_true_to_le.reflexivity
 457   ]
 458 qed.
 459
 460 theorem not_bertrand_to_le_B:
 461 \forall n.exp 2 7 \le n \to not_bertrand n \to
 462 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 463 intros.
 464 rewrite > eq_B_B1.
 465 rewrite > eq_B1_times_B_split1_B_split2.
 466 apply le_times
 467   [apply (trans_le ? (teta ((2*n)/3)))
 468     [apply le_B_split1_teta
 469       [apply (trans_le ? ? ? ? H).
 470        apply leb_true_to_le.reflexivity
 471       |assumption
 472       ]
 473     |apply le_teta
 474     ]
 475   |apply le_B_split2_exp.
 476    assumption
 477   ]
 478 qed.
 479
 480 (*
 481 theorem not_bertrand_to_le1:
 482 \forall n.18 \le n \to not_bertrand n \to
 483 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
 484 *)
 485
 486 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
 487 intros.
 488 rewrite > (div_mod n m) in ⊢ (? ? %)
 489   [apply le_plus_n_r
 490   |assumption
 491   ]
 492 qed.
 493
 494 theorem not_bertrand_to_le1:
 495 \forall n.exp 2 7 \le n \to not_bertrand n \to
 496 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
 497 intros.
 498 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
 499   [apply lt_O_exp.apply lt_O_S
 500   |rewrite < exp_plus_times.
 501    apply (trans_le ? (exp 2 (2*n)))
 502     [apply le_exp
 503       [apply lt_O_S
 504       |rewrite < sym_plus.
 505        change in ⊢ (? % ?) with (3*(2*n/3)).
 506        rewrite > sym_times.
 507        apply le_times_div_m_m.
 508        apply lt_O_S
 509       ]
 510 (* weaker form
 511        rewrite < distr_times_plus.
 512        apply le_times_r.
 513        apply (trans_le ? ((2*n + n)/3))
 514         [apply le_plus_div.apply lt_O_S
 515         |rewrite < sym_plus.
 516          change in ⊢ (? (? % ?) ?) with (3*n).
 517          rewrite < sym_times.
 518          rewrite > lt_O_to_div_times
 519           [apply le_n
 520           |apply lt_O_S
 521           ]
 522         ]
 523       ] *)
 524     |apply (trans_le ? (2*n*B(2*n)))
 525       [apply le_exp_B.
 526        apply (trans_le ? ? ? ? H).
 527        apply leb_true_to_le.reflexivity
 528       |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
 529         [rewrite > exp_S.
 530          rewrite < assoc_times.
 531          rewrite < sym_times in ⊢ (? ? (? % ?)).
 532          rewrite > assoc_times in ⊢ (? ? %).
 533          apply le_times_r.
 534          apply not_bertrand_to_le_B;assumption
 535         |apply le_times_to_le_div
 536           [apply lt_O_S
 537           |apply (trans_le ? (sqrt (exp 2 8)))
 538             [apply leb_true_to_le.reflexivity
 539             |apply monotonic_sqrt.
 540              change in ⊢ (? % ?) with (2*(exp 2 7)).
 541              apply le_times_r.
 542              assumption
 543             ]
 544           ]
 545         ]
 546       ]
 547     ]
 548   ]
 549 qed.
 550
 551 theorem not_bertrand_to_le2:
 552 \forall n.exp 2 7 \le n \to not_bertrand n \to
 553 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
 554 intros.
 555 rewrite < (eq_log_exp 2)
 556   [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
 557     [apply le_log
 558       [apply le_n
 559       |apply not_bertrand_to_le1;assumption
 560       ]
 561     |apply log_exp1.
 562      apply le_n
 563     ]
 564   |apply le_n
 565   ]
 566 qed.
 567
 568 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
 569 (a/b)*(c/d) \le (a*c)/(b*d).
 570 intros.
 571 apply le_times_to_le_div
 572   [rewrite > (times_n_O O).
 573    apply lt_times;assumption
 574   |rewrite > assoc_times.
 575    rewrite < assoc_times in ⊢ (? (? ? %) ?).
 576    rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
 577    rewrite > assoc_times.
 578    rewrite < assoc_times.
 579    apply le_times;
 580    rewrite > sym_times;apply le_times_div_m_m;assumption
 581   ]
 582 qed.
 583
 584 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
 585 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
 586 intros.
 587 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
 588   [rewrite > sym_times.
 589    apply le_times_to_le_div
 590     [apply lt_O_S
 591     |rewrite < assoc_times.
 592      apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
 593       [apply le_times_l.assumption
 594       |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
 595         [apply le_times_div_div_times.
 596          apply lt_O_S
 597         |rewrite > assoc_times.
 598          rewrite > sym_times.
 599          rewrite > lt_O_to_div_times.
 600          apply leq_sqrt_n.
 601          apply lt_O_S
 602         ]
 603       ]
 604     ]
 605   |change in ⊢ (? (? % ?) ?) with (2*2).
 606    rewrite > assoc_times.
 607    apply le_times_r.
 608    assumption
 609   ]
 610 qed.
 611
 612 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
 613 n/(S m) < n/m.
 614 intros.
 615 apply lt_times_to_lt_div.
 616 apply (lt_to_le_to_lt ? (S(n/m)*m))
 617   [apply lt_div_S.assumption
 618   |rewrite > sym_times in ⊢ (? ? %). simplify.
 619    rewrite > sym_times in ⊢ (? ? (? ? %)).
 620    apply le_plus_l.
 621    apply le_times_to_le_div
 622     [assumption
 623     |rewrite < exp_SSO.
 624      assumption
 625     ]
 626   ]
 627 qed.
 628
 629 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
 630 intros.
 631 rewrite > exp_SSO.
 632 rewrite > distr_times_plus.
 633 rewrite > times_plus_l.
 634 rewrite < exp_SSO.
 635 rewrite > assoc_plus.
 636 rewrite > assoc_plus.
 637 apply eq_f.
 638 rewrite > times_plus_l.
 639 rewrite < exp_SSO.
 640 rewrite < assoc_plus.
 641 rewrite < sym_times.
 642 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
 643 rewrite > assoc_times.
 644 apply eq_f2;reflexivity.
 645 qed.
 646
 647 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
 648 intros.
 649 lapply (le_log 2 ? ? (le_n ?) H) as H1.
 650 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
 651 rewrite > log_exp
 652   [rewrite > sym_plus.
 653    rewrite > plus_n_Sm.
 654    unfold sqrt.
 655    apply f_m_to_le_max
 656     [apply le_times_r.
 657      apply (trans_le ? (2*log 2 n))
 658       [rewrite < times_SSO_n.
 659        apply le_plus_r.
 660        apply (trans_le ? 8)
 661         [apply leb_true_to_le.reflexivity
 662         |rewrite < (eq_log_exp 2)
 663           [assumption
 664           |apply le_n
 665           ]
 666         ]
 667       |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
 668        apply le_times_SSO_n_exp_SSO_n.
 669        apply (lt_to_le_to_lt ? ? ? ? H).
 670        apply leb_true_to_le.reflexivity
 671       ]
 672     |apply le_to_leb_true.
 673      rewrite > assoc_times.
 674      apply le_times_r.
 675      rewrite > sym_times.
 676      rewrite > assoc_times.
 677      rewrite < exp_SSO.
 678      rewrite > exp_plus_SSO.
 679      rewrite > distr_times_plus.
 680      rewrite > distr_times_plus.
 681      rewrite > assoc_plus.
 682      apply (trans_le ? (4*exp (log 2 n) 2))
 683       [change in ⊢ (? ? (? % ?)) with (2*2).
 684        rewrite > assoc_times in ⊢ (? ? %).
 685        rewrite < times_SSO_n in ⊢ (? ? %).
 686        apply le_plus_r.
 687        rewrite < times_SSO_n in ⊢ (? ? %).
 688        apply le_plus
 689         [rewrite > sym_times in ⊢ (? (? ? %) ?).
 690          rewrite < assoc_times.
 691          rewrite < assoc_times.
 692          change in ⊢ (? (? % ?) ?) with 8.
 693          rewrite > exp_SSO.
 694          apply le_times_l.
 695          (* strange things here *)
 696          rewrite < (eq_log_exp 2)
 697           [assumption
 698           |apply le_n
 699           ]
 700         |apply (trans_le ? (log 2 n))
 701           [change in ⊢ (? % ?) with 8.
 702            rewrite < (eq_log_exp 2)
 703             [assumption
 704             |apply le_n
 705             ]
 706           |rewrite > exp_n_SO in ⊢ (? % ?).
 707            apply le_exp
 708             [apply lt_O_log
 709               [apply (lt_to_le_to_lt ? ? ? ? H).
 710                apply leb_true_to_le.reflexivity
 711               |apply (lt_to_le_to_lt ? ? ? ? H).
 712                apply leb_true_to_le.reflexivity
 713               ]
 714             |apply le_n_Sn
 715             ]
 716           ]
 717         ]
 718       |change in ⊢ (? (? % ?) ?) with (exp 2 2).
 719        apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
 720         [apply le_times_exp_n_SSO_exp_SSO_n
 721           [apply le_n
 722           |change in ⊢ (? % ?) with 8.
 723            rewrite < (eq_log_exp 2)
 724             [assumption
 725             |apply le_n
 726             ]
 727           ]
 728         |apply (lt_to_le_to_lt ? ? ? ? H).
 729          apply leb_true_to_le.reflexivity
 730         ]
 731       ]
 732     ]
 733   |apply le_n
 734   |apply (lt_to_le_to_lt ? ? ? ? H).
 735    apply leb_true_to_le.reflexivity
 736   ]
 737 qed.
 738
 739 theorem le_to_bertrand:
 740 \forall n. (exp 2 8) \le n \to bertrand n.
 741 intros.
 742 apply not_not_bertrand_to_bertrand.unfold.intro.
 743 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
 744   [apply not_bertrand_to_le2
 745     [apply (trans_le ? ? ? ? H).
 746      apply le_exp
 747       [apply lt_O_S
 748       |apply le_n_Sn
 749       ]
 750     |assumption
 751     ]
 752   |apply lt_to_not_le.
 753    apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
 754     [apply tech.apply tech3.assumption
 755     |apply lt_O_S
 756     |apply (trans_le ? (2*exp 2 8))
 757       [apply leb_true_to_le.reflexivity
 758       |apply le_times_r.assumption
 759       ]
 760     ]
 761   ]
 762 qed.
 763
 764 (* test
 765 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
 766 reflexivity.
 767 *)