matita/matita/lib/arithmetics/chebyshev/bertrand256.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/chebyshev/chebyshev_teta.ma".
  13
  14 (* include "nat/sqrt.ma".
  15 include "nat/chebyshev_teta.ma".
  16 include "nat/chebyshev.ma".
  17 include "list/in.ma".
  18 include "list/sort.ma".
  19 include "nat/o.ma".
  20 include "nat/sieve.ma". *)
  21
  22 (*
  23 let rec list_divides l n \def
  24   match l with
  25   [ nil ⇒ false
  26   | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
  27
  28 definition lprim : nat \to list nat \def
  29   \lambda n.let rec aux m acc \def
  30      match m with
  31      [ O => acc
  32      | S m1 => match (list_divides acc (n-m1)) with
  33        [ true => aux m1 acc
  34        | false => aux m1 (n-m1::acc)]]
  35   in aux (pred n) [].
  36
  37 let rec checker l \def
  38     match l with
  39       [ nil => true
  40       | cons h1 t1 => match t1 with
  41          [ nil => true
  42          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
  43
  44 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
  45 intros 2;simplify;intro;elim l in H ⊢ %
  46   [reflexivity
  47   |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
  48    apply (andb_true_true ? ? H1)]
  49 qed.
  50
  51 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
  52                         checker l = true \to x \leq 2*y.
  53 intro;elim l1 0
  54   [simplify;intros 5;rewrite > H;simplify;intro;
  55    apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
  56   |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
  57    apply (H l2 ? ? ? ? Hletin);reflexivity]
  58 qed.
  59 *)
  60
  61 definition bertrand ≝ λn. ∃p.n < p ∧ p \le 2*n ∧ (prime p).
  62
  63 definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → \not (prime p).
  64
  65 lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧
  66                  ∀q.prime q → q < p → q ≤ n.
  67 #n cases (le_to_or_lt_eq ?? (le_O_n n)) #Hn
  68   [%{(min (S (n!)) (S n) primeb)} %
  69     [%[@le_min_l
  70       |@primeb_true_to_prime @(f_min_true primeb)
  71        cases (ex_prime n Hn) #p * * #ltnp #lep #primep
  72        %{p} %
  73         [% [@ltnp | whd >(plus_n_O p) >plus_n_Sm @le_plus //]
  74         |@prime_to_primeb_true //
  75         ]
  76       ]
  77     |#p #primep #ltp @not_lt_to_le % #ltnp
  78      lapply (lt_min_to_false … ltnp ltp)
  79      >(prime_to_primeb_true ? primep) #H destruct (H)
  80     ]
  81   |%{2} %
  82     [%[<Hn @lt_O_S | @primeb_true_to_prime //]
  83     |#p #primep #lt2 @False_ind @(absurd … lt2)
  84      @le_to_not_lt @prime_to_lt_SO //
  85     ]
  86   ]
  87 qed.
  88
  89 theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
  90 list_of_primes pn l  \to
  91 (\forall p. prime p \to p \le pn \to in_list nat p l) \to
  92 (\forall p. in_list nat p l \to 2 < p \to
  93 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
  94 intros.
  95 elim (min_prim n).
  96 apply (ex_intro ? ? a).
  97 elim H6.clear H6.elim H7.clear H7.
  98 split
  99   [split
 100     [assumption
 101     |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
 102       [elim (H5 a)
 103         [elim H10.clear H10.elim H11.clear H11.
 104          apply (trans_le ? ? ? H12).
 105          apply le_times_r.
 106          apply H8
 107           [unfold in H3.
 108            elim (H3 a1 H10).
 109            assumption
 110           |assumption
 111           ]
 112         |apply H4
 113           [assumption
 114           |apply not_lt_to_le.intro.
 115            apply (lt_to_not_le ? ? H2).
 116            apply H8;assumption
 117           ]
 118         |assumption
 119         ]
 120       |rewrite < H7.
 121        apply O_lt_const_to_le_times_const.
 122        assumption
 123       ]
 124     ]
 125   |assumption
 126   ]
 127 qed.
 128
 129 let rec check_list l \def
 130   match l with
 131   [ nil \Rightarrow true
 132   | cons (hd:nat) tl \Rightarrow
 133     match tl with
 134      [ nil \Rightarrow eqb hd 2
 135      | cons hd1 tl1 \Rightarrow
 136       (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
 137     ]
 138   ]
 139 .
 140
 141 lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
 142 m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
 143 intros 3.
 144 change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
 145 intro.
 146 lapply (andb_true_true ? ? H) as H1.
 147 lapply (andb_true_true_r ? ? H) as H2.clear H.
 148 lapply (andb_true_true ? ? H1) as H3.
 149 lapply (andb_true_true_r ? ? H1) as H4.clear H1.
 150 split
 151   [split
 152     [split
 153       [apply leb_true_to_le.assumption
 154       |apply leb_true_to_le.assumption
 155       ]
 156     |assumption
 157     ]
 158   |generalize in match H2.
 159    cases l
 160     [intro.reflexivity
 161     |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
 162      intro.
 163      lapply (andb_true_true_r ? ? H) as H2.
 164      assumption
 165     ]
 166   ]
 167 qed.
 168
 169 theorem check_list2: \forall l. check_list l = true \to
 170 \forall p. in_list nat p l \to 2 < p \to
 171 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
 172 intro.elim l 2
 173   [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
 174   |cases l1;intros
 175     [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
 176      apply False_ind.
 177      apply (lt_to_not_eq ? ? H3).
 178      apply sym_eq.apply eqb_true_to_eq.
 179      rewrite > H4.apply H1
 180     |elim (check_list1 ? ? ? H1).clear H1.
 181      elim H4.clear H4.
 182      elim H1.clear H1.
 183      elim (in_list_cons_case ? ? ? ? H2)
 184       [apply (ex_intro ? ? n).
 185        split
 186         [split
 187           [apply in_list_cons.apply in_list_head
 188           |rewrite > H1.assumption
 189           ]
 190         |rewrite > H1.assumption
 191         ]
 192       |elim (H H6 p H1 H3).clear H.
 193        apply (ex_intro ? ? a1).
 194        elim H8.clear H8.
 195        elim H.clear H.
 196        split
 197         [split
 198           [apply in_list_cons.assumption
 199           |assumption
 200           ]
 201         |assumption
 202         ]
 203       ]
 204     ]
 205   ]
 206 qed.
 207
 208 (* qualcosa che non va con gli S *)
 209 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 210 intros.
 211 apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
 212   [assumption
 213   |apply primeb_true_to_prime.reflexivity
 214   |apply (le_to_lt_to_lt ? ? ? H1).
 215    apply le_n
 216   |lapply (sieve_sound1 (S(exp 2 8))) as H
 217     [elim H.assumption
 218     |apply leb_true_to_le.reflexivity
 219     ]
 220   |intros.apply (sieve_sound2 ? ? H3 H2)
 221   |apply check_list2.
 222    reflexivity
 223   ]
 224 qed.
 225
 226 lemma not_not_bertrand_to_bertrand1: \forall n.
 227 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
 228 (\forall p.x < p \to p \le 2*n \to \not (prime p))
 229 \to \exists p.n < p \land p \le  x \land (prime p).
 230 intros 4.elim H1
 231   [apply False_ind.apply H.assumption
 232   |apply (bool_elim ? (primeb (S n1)));intro
 233     [apply (ex_intro ? ? (S n1)).
 234      split
 235       [split
 236         [apply le_S_S.assumption
 237         |apply le_n
 238         ]
 239       |apply primeb_true_to_prime.assumption
 240       ]
 241     |elim H3
 242       [elim H7.clear H7.
 243        elim H8.clear H8.
 244        apply (ex_intro ? ? a).
 245        split
 246         [split
 247           [assumption
 248           |apply le_S.assumption
 249           ]
 250         |assumption
 251         ]
 252       |apply lt_to_le.assumption
 253       |elim (le_to_or_lt_eq ? ? H7)
 254         [apply H5;assumption
 255         |rewrite < H9.
 256          apply primeb_false_to_not_prime.
 257          assumption
 258         ]
 259       ]
 260     ]
 261   ]
 262 qed.
 263
 264 theorem not_not_bertrand_to_bertrand: \forall n.
 265 \lnot (not_bertrand n) \to bertrand n.
 266 unfold bertrand.intros.
 267 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
 268   [assumption
 269   |apply le_times_n.apply le_n_Sn
 270   |apply le_n
 271   |intros.apply False_ind.
 272    apply (lt_to_not_le ? ? H1 H2)
 273   ]
 274 qed.
 275
 276
 277
 278 definition k \def \lambda n,p.
 279 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
 280
 281 theorem le_k: \forall n,p. k n p \le log p n.
 282 intros.unfold k.elim (log p n)
 283   [apply le_n
 284   |rewrite > true_to_sigma_p_Sn
 285     [rewrite > plus_n_SO.
 286      rewrite > sym_plus in ⊢ (? ? %).
 287      apply le_plus
 288       [apply le_S_S_to_le.
 289        apply lt_mod_m_m.
 290        apply lt_O_S
 291       |assumption
 292       ]
 293     |reflexivity
 294     ]
 295   ]
 296 qed.
 297
 298 definition B1 \def
 299 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
 300
 301 theorem eq_B_B1: \forall n. B n = B1 n.
 302 intros.unfold B.unfold B1.
 303 apply eq_pi_p
 304   [intros.reflexivity
 305   |intros.unfold k.
 306    apply exp_sigma_p1
 307   ]
 308 qed.
 309
 310 definition B_split1 \def \lambda n.
 311 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
 312
 313 definition B_split2 \def \lambda n.
 314 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
 315
 316 theorem eq_B1_times_B_split1_B_split2: \forall n.
 317 B1 n = B_split1 n * B_split2 n.
 318 intro.unfold B1.unfold B_split1.unfold B_split2.
 319 rewrite < times_pi_p.
 320 apply eq_pi_p
 321   [intros.reflexivity
 322   |intros.apply (bool_elim ? (leb (k n x) 1));intro
 323     [rewrite > (lt_to_leb_false 2 (k n x))
 324       [simplify.rewrite < plus_n_O.
 325        rewrite < times_n_SO.reflexivity
 326       |apply le_S_S.apply leb_true_to_le.assumption
 327       ]
 328     |rewrite > (le_to_leb_true 2 (k n x))
 329       [simplify.rewrite < plus_n_O.
 330        rewrite < plus_n_O.reflexivity
 331       |apply not_le_to_lt.apply leb_false_to_not_le.assumption
 332       ]
 333     ]
 334   ]
 335 qed.
 336
 337 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
 338 intros.
 339 cut (O < m) as H2
 340   [apply not_le_to_lt.
 341    intro.apply (lt_to_not_le ? ? H1).
 342    apply le_times_to_le_div;assumption
 343   |apply (ltn_to_ltO ? ? H1)
 344   ]
 345 qed.
 346
 347 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
 348 intros.
 349 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 350   [apply div_mod_spec_div_mod.
 351    apply (ltn_to_ltO ? ? H)
 352   |apply div_mod_spec_intro
 353     [assumption
 354     |reflexivity
 355     ]
 356   ]
 357 qed.
 358
 359 (* the value of n could be smaller *)
 360 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
 361 intros.unfold k.
 362 elim (log p (2*n))
 363   [reflexivity
 364   |rewrite > true_to_sigma_p_Sn
 365     [rewrite > H3.
 366      rewrite < plus_n_O.
 367      cases n1
 368       [rewrite < exp_n_SO.
 369        cut (2*n/p = 2) as H4
 370         [rewrite > H4.reflexivity
 371         |apply lt_to_le_times_to_lt_S_to_div
 372           [apply (ltn_to_ltO ? ? H2)
 373           |rewrite < sym_times.
 374            apply le_times_r.
 375            assumption
 376           |rewrite > sym_times in ⊢ (? ? %).
 377            apply lt_div_to_times
 378             [apply lt_O_S
 379             |assumption
 380             ]
 381           ]
 382         ]
 383       |cut (2*n/(p)\sup(S (S n2)) = O) as H4
 384         [rewrite > H4.reflexivity
 385         |apply lt_to_div_O.
 386          apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 387           [apply (le_times_to_le (exp 3 2))
 388             [apply leb_true_to_le.reflexivity
 389             |rewrite > sym_times in ⊢ (? ? %).
 390              rewrite > times_exp.
 391              apply (trans_le ? (exp n 2))
 392               [rewrite < assoc_times.
 393                rewrite > exp_SSO in ⊢ (? ? %).
 394                apply le_times_l.
 395                assumption
 396               |apply monotonic_exp1.
 397                apply (le_plus_to_le 3).
 398                change in ⊢ (? ? %) with ((S(2*n/3))*3).
 399                apply (trans_le ? (2*n))
 400                 [simplify in ⊢ (? ? %).
 401                  rewrite < plus_n_O.
 402                  apply le_plus_l.
 403                  apply (trans_le ? 18 ? ? H).
 404                  apply leb_true_to_le.reflexivity
 405                 |apply lt_to_le.
 406                  apply lt_div_S.
 407                  apply lt_O_S
 408                 ]
 409               ]
 410             ]
 411           |apply (lt_to_le_to_lt ? (exp p 2))
 412             [apply lt_exp1
 413               [apply lt_O_S
 414               |assumption
 415               ]
 416             |apply le_exp
 417               [apply (ltn_to_ltO ? ? H2)
 418               |apply le_S_S.apply le_S_S.apply le_O_n
 419               ]
 420             ]
 421           ]
 422         ]
 423       ]
 424     |reflexivity
 425     ]
 426   ]
 427 qed.
 428
 429 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 430 B_split1 (2*n) \le teta (2 * n / 3).
 431 intros. unfold B_split1.unfold teta.
 432 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 433   [apply le_pi_p.intros.
 434    apply le_exp
 435     [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
 436     |apply (bool_elim ? (leb (k (2*n) i) 1));intro
 437       [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
 438         [lapply (le_S_S_to_le ? ? H5) as H6.
 439          apply (le_n_O_elim ? H6).
 440          rewrite < times_n_O.
 441          apply le_n
 442         |rewrite > (eq_to_eqb_true ? ? H5).
 443          rewrite > H5.apply le_n
 444         ]
 445       |apply le_O_n
 446       ]
 447     ]
 448   |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 449     [apply (eq_ind ? ? ? (le_n ?)).
 450      apply or_false_eq_SO_to_eq_pi_p
 451       [apply le_S_S.
 452        apply le_times_to_le_div2
 453         [apply lt_O_S
 454         |rewrite > sym_times in ⊢ (? ? %).
 455          apply le_times_n.
 456          apply leb_true_to_le.reflexivity
 457         ]
 458       |intros.
 459        unfold not_bertrand in H1.
 460        elim (decidable_le (S n) i)
 461         [left.
 462          apply not_prime_to_primeb_false.
 463          apply H1
 464           [assumption
 465           |apply le_S_S_to_le.assumption
 466           ]
 467         |right.
 468          rewrite > k1
 469           [reflexivity
 470           |assumption
 471           |apply le_S_S_to_le.
 472            apply not_le_to_lt.assumption
 473           |assumption
 474           ]
 475         ]
 476       ]
 477     |apply le_pi_p.intros.
 478      elim (eqb (k (2*n) i) 1)
 479       [rewrite < exp_n_SO.apply le_n
 480       |simplify.apply prime_to_lt_O.
 481        apply primeb_true_to_prime.
 482        assumption
 483       ]
 484     ]
 485   ]
 486 qed.
 487
 488 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
 489 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
 490 intros.unfold B_split2.
 491 cut (O < n)
 492   [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
 493         (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
 494     [apply (eq_ind ? ? ? (le_n ?)).
 495      apply or_false_eq_SO_to_eq_pi_p
 496       [apply le_S_S.
 497        apply le_sqrt_n_n
 498       |intros.
 499        apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 500         [apply False_ind.
 501          apply (lt_to_not_le ? ? H1).unfold sqrt.
 502          apply f_m_to_le_max
 503           [apply le_S_S_to_le.assumption
 504           |apply le_to_leb_true.
 505            rewrite < exp_SSO.
 506            apply not_lt_to_le.intro.
 507            apply (le_to_not_lt 2 (log i (2*n)))
 508             [apply (trans_le ? (k (2*n) i))
 509               [apply leb_true_to_le.assumption
 510               |apply le_k
 511               ]
 512             |apply le_S_S.unfold log.apply f_false_to_le_max
 513               [apply (ex_intro ? ? O).split
 514                 [apply le_O_n
 515                 |apply le_to_leb_true.simplify.
 516                  apply (trans_le ? n)
 517                   [assumption.
 518                   |apply le_plus_n_r
 519                   ]
 520                 ]
 521               |intros.apply lt_to_leb_false.
 522                apply (lt_to_le_to_lt ? (exp i 2))
 523                 [assumption
 524                 |apply le_exp
 525                   [apply (ltn_to_ltO ? ? H1)
 526                   |assumption
 527                   ]
 528                 ]
 529               ]
 530             ]
 531           ]
 532         |right.reflexivity
 533         ]
 534       ]
 535     |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
 536       [apply le_pi_p.intros.
 537        apply (trans_le ? (exp i (log i (2*n))))
 538         [apply le_exp
 539           [apply prime_to_lt_O.
 540            apply primeb_true_to_prime.
 541            assumption
 542           |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 543             [simplify in ⊢ (? (? % ?) ?).
 544              rewrite > sym_times.
 545              rewrite < times_n_SO.
 546              apply le_k
 547             |apply le_O_n
 548             ]
 549           ]
 550         |apply le_exp_log.
 551          rewrite > (times_n_O O) in ⊢ (? % ?).
 552          apply lt_times
 553           [apply lt_O_S
 554           |assumption
 555           ]
 556         ]
 557       |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
 558         [unfold prim.
 559          apply (eq_ind ? ? ? (le_n ?)).
 560          apply exp_sigma_p
 561         |apply le_exp
 562           [rewrite > (times_n_O O) in ⊢ (? % ?).
 563            apply lt_times
 564             [apply lt_O_S
 565             |assumption
 566             ]
 567           |apply le_prim_n3.
 568            unfold sqrt.
 569            apply f_m_to_le_max
 570             [apply (trans_le ? (2*(exp 2 7)))
 571               [apply leb_true_to_le.reflexivity
 572               |apply le_times_r.assumption
 573               ]
 574             |apply le_to_leb_true.
 575              apply (trans_le ? (2*(exp 2 7)))
 576               [apply leb_true_to_le.reflexivity
 577               |apply le_times_r.assumption
 578               ]
 579             ]
 580           ]
 581         ]
 582       ]
 583     ]
 584   |apply (lt_to_le_to_lt ? ? ? ? H).
 585    apply leb_true_to_le.reflexivity
 586   ]
 587 qed.
 588
 589 theorem not_bertrand_to_le_B:
 590 \forall n.exp 2 7 \le n \to not_bertrand n \to
 591 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 592 intros.
 593 rewrite > eq_B_B1.
 594 rewrite > eq_B1_times_B_split1_B_split2.
 595 apply le_times
 596   [apply (trans_le ? (teta ((2*n)/3)))
 597     [apply le_B_split1_teta
 598       [apply (trans_le ? ? ? ? H).
 599        apply leb_true_to_le.reflexivity
 600       |assumption
 601       ]
 602     |apply le_teta
 603     ]
 604   |apply le_B_split2_exp.
 605    assumption
 606   ]
 607 qed.
 608
 609 (*
 610 theorem not_bertrand_to_le1:
 611 \forall n.18 \le n \to not_bertrand n \to
 612 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
 613 *)
 614
 615 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
 616 intros.
 617 rewrite > (div_mod n m) in ⊢ (? ? %)
 618   [apply le_plus_n_r
 619   |assumption
 620   ]
 621 qed.
 622
 623 theorem not_bertrand_to_le1:
 624 \forall n.exp 2 7 \le n \to not_bertrand n \to
 625 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
 626 intros.
 627 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
 628   [apply lt_O_exp.apply lt_O_S
 629   |rewrite < exp_plus_times.
 630    apply (trans_le ? (exp 2 (2*n)))
 631     [apply le_exp
 632       [apply lt_O_S
 633       |rewrite < sym_plus.
 634        change in ⊢ (? % ?) with (3*(2*n/3)).
 635        rewrite > sym_times.
 636        apply le_times_div_m_m.
 637        apply lt_O_S
 638       ]
 639     |apply (trans_le ? (2*n*B(2*n)))
 640       [apply le_exp_B.
 641        apply (trans_le ? ? ? ? H).
 642        apply leb_true_to_le.reflexivity
 643       |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
 644         [rewrite > exp_S.
 645          rewrite < assoc_times.
 646          rewrite < sym_times in ⊢ (? ? (? % ?)).
 647          rewrite > assoc_times in ⊢ (? ? %).
 648          apply le_times_r.
 649          apply not_bertrand_to_le_B;assumption
 650         |apply le_times_to_le_div
 651           [apply lt_O_S
 652           |apply (trans_le ? (sqrt (exp 2 8)))
 653             [apply leb_true_to_le.reflexivity
 654             |apply monotonic_sqrt.
 655              change in ⊢ (? % ?) with (2*(exp 2 7)).
 656              apply le_times_r.
 657              assumption
 658             ]
 659           ]
 660         ]
 661       ]
 662     ]
 663   ]
 664 qed.
 665
 666 theorem not_bertrand_to_le2:
 667 \forall n.exp 2 7 \le n \to not_bertrand n \to
 668 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
 669 intros.
 670 rewrite < (eq_log_exp 2)
 671   [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
 672     [apply le_log
 673       [apply le_n
 674       |apply not_bertrand_to_le1;assumption
 675       ]
 676     |apply log_exp1.
 677      apply le_n
 678     ]
 679   |apply le_n
 680   ]
 681 qed.
 682
 683 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
 684 (a/b)*(c/d) \le (a*c)/(b*d).
 685 intros.
 686 apply le_times_to_le_div
 687   [rewrite > (times_n_O O).
 688    apply lt_times;assumption
 689   |rewrite > assoc_times.
 690    rewrite < assoc_times in ⊢ (? (? ? %) ?).
 691    rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
 692    rewrite > assoc_times.
 693    rewrite < assoc_times.
 694    apply le_times;
 695    rewrite > sym_times;apply le_times_div_m_m;assumption
 696   ]
 697 qed.
 698
 699 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
 700 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
 701 intros.
 702 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
 703   [rewrite > sym_times.
 704    apply le_times_to_le_div
 705     [apply lt_O_S
 706     |rewrite < assoc_times.
 707      apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
 708       [apply le_times_l.assumption
 709       |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
 710         [apply le_times_div_div_times.
 711          apply lt_O_S
 712         |rewrite > assoc_times.
 713          rewrite > sym_times.
 714          rewrite > lt_O_to_div_times.
 715          apply leq_sqrt_n.
 716          apply lt_O_S
 717         ]
 718       ]
 719     ]
 720   |change in ⊢ (? (? % ?) ?) with (2*2).
 721    rewrite > assoc_times.
 722    apply le_times_r.
 723    assumption
 724   ]
 725 qed.
 726
 727 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
 728 n/(S m) < n/m.
 729 intros.
 730 apply lt_times_to_lt_div.
 731 apply (lt_to_le_to_lt ? (S(n/m)*m))
 732   [apply lt_div_S.assumption
 733   |rewrite > sym_times in ⊢ (? ? %). simplify.
 734    rewrite > sym_times in ⊢ (? ? (? ? %)).
 735    apply le_plus_l.
 736    apply le_times_to_le_div
 737     [assumption
 738     |rewrite < exp_SSO.
 739      assumption
 740     ]
 741   ]
 742 qed.
 743
 744 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
 745 intros.
 746 rewrite > exp_SSO.
 747 rewrite > distr_times_plus.
 748 rewrite > times_plus_l.
 749 rewrite < exp_SSO.
 750 rewrite > assoc_plus.
 751 rewrite > assoc_plus.
 752 apply eq_f.
 753 rewrite > times_plus_l.
 754 rewrite < exp_SSO.
 755 rewrite < assoc_plus.
 756 rewrite < sym_times.
 757 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
 758 rewrite > assoc_times.
 759 apply eq_f2;reflexivity.
 760 qed.
 761
 762 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
 763 intros.
 764 lapply (le_log 2 ? ? (le_n ?) H) as H1.
 765 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
 766 rewrite > log_exp
 767   [rewrite > sym_plus.
 768    rewrite > plus_n_Sm.
 769    unfold sqrt.
 770    apply f_m_to_le_max
 771     [apply le_times_r.
 772      apply (trans_le ? (2*log 2 n))
 773       [rewrite < times_SSO_n.
 774        apply le_plus_r.
 775        apply (trans_le ? 8)
 776         [apply leb_true_to_le.reflexivity
 777         |rewrite < (eq_log_exp 2)
 778           [assumption
 779           |apply le_n
 780           ]
 781         ]
 782       |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
 783        apply le_times_SSO_n_exp_SSO_n.
 784        apply (lt_to_le_to_lt ? ? ? ? H).
 785        apply leb_true_to_le.reflexivity
 786       ]
 787     |apply le_to_leb_true.
 788      rewrite > assoc_times.
 789      apply le_times_r.
 790      rewrite > sym_times.
 791      rewrite > assoc_times.
 792      rewrite < exp_SSO.
 793      rewrite > exp_plus_SSO.
 794      rewrite > distr_times_plus.
 795      rewrite > distr_times_plus.
 796      rewrite > assoc_plus.
 797      apply (trans_le ? (4*exp (log 2 n) 2))
 798       [change in ⊢ (? ? (? % ?)) with (2*2).
 799        rewrite > assoc_times in ⊢ (? ? %).
 800        rewrite < times_SSO_n in ⊢ (? ? %).
 801        apply le_plus_r.
 802        rewrite < times_SSO_n in ⊢ (? ? %).
 803        apply le_plus
 804         [rewrite > sym_times in ⊢ (? (? ? %) ?).
 805          rewrite < assoc_times.
 806          rewrite < assoc_times.
 807          change in ⊢ (? (? % ?) ?) with 8.
 808          rewrite > exp_SSO.
 809          apply le_times_l.
 810          (* strange things here *)
 811          rewrite < (eq_log_exp 2)
 812           [assumption
 813           |apply le_n
 814           ]
 815         |apply (trans_le ? (log 2 n))
 816           [change in ⊢ (? % ?) with 8.
 817            rewrite < (eq_log_exp 2)
 818             [assumption
 819             |apply le_n
 820             ]
 821           |rewrite > exp_n_SO in ⊢ (? % ?).
 822            apply le_exp
 823             [apply lt_O_log
 824               [apply (lt_to_le_to_lt ? ? ? ? H).
 825                apply leb_true_to_le.reflexivity
 826               |apply (lt_to_le_to_lt ? ? ? ? H).
 827                apply leb_true_to_le.reflexivity
 828               ]
 829             |apply le_n_Sn
 830             ]
 831           ]
 832         ]
 833       |change in ⊢ (? (? % ?) ?) with (exp 2 2).
 834        apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
 835         [apply le_times_exp_n_SSO_exp_SSO_n
 836           [apply le_n
 837           |change in ⊢ (? % ?) with 8.
 838            rewrite < (eq_log_exp 2)
 839             [assumption
 840             |apply le_n
 841             ]
 842           ]
 843         |apply (lt_to_le_to_lt ? ? ? ? H).
 844          apply leb_true_to_le.reflexivity
 845         ]
 846       ]
 847     ]
 848   |apply le_n
 849   |apply (lt_to_le_to_lt ? ? ? ? H).
 850    apply leb_true_to_le.reflexivity
 851   ]
 852 qed.
 853
 854 theorem le_to_bertrand2:
 855 \forall n. (exp 2 8) \le n \to bertrand n.
 856 intros.
 857 apply not_not_bertrand_to_bertrand.unfold.intro.
 858 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
 859   [apply not_bertrand_to_le2
 860     [apply (trans_le ? ? ? ? H).
 861      apply le_exp
 862       [apply lt_O_S
 863       |apply le_n_Sn
 864       ]
 865     |assumption
 866     ]
 867   |apply lt_to_not_le.
 868    apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
 869     [apply tech.apply tech3.assumption
 870     |apply lt_O_S
 871     |apply (trans_le ? (2*exp 2 8))
 872       [apply leb_true_to_le.reflexivity
 873       |apply le_times_r.assumption
 874       ]
 875     ]
 876   ]
 877 qed.
 878
 879 theorem bertrand_n :
 880 \forall n. O < n \to bertrand n.
 881 intros;elim (decidable_le n 256)
 882   [apply le_to_bertrand;assumption
 883   |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
 884 qed.
 885
 886 (* test
 887 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
 888 reflexivity.
 889 *)