matita/matita/lib/arithmetics/chebyshev/bertrand.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/sqrt.ma".
  13 include "arithmetics/chebyshev/psi_bounds.ma".
  14 include "arithmetics/chebyshev/chebyshev_theta.ma".
  15
  16 definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p.
  17
  18 definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → ¬(prime p).
  19
  20 lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧
  21                  ∀q.prime q → q < p → q ≤ n.
  22 #n cases (le_to_or_lt_eq ?? (le_O_n n)) #Hn
  23   [%{(min (S (n!)) (S n) primeb)} %
  24     [%[@le_min_l
  25       |@primeb_true_to_prime @(f_min_true primeb)
  26        cases (ex_prime n Hn) #p * * #ltnp #lep #primep
  27        %{p} %
  28         [% [@ltnp | whd >(plus_n_O p) >plus_n_Sm @le_plus //]
  29         |@prime_to_primeb_true //
  30         ]
  31       ]
  32     |#p #primep #ltp @not_lt_to_le % #ltnp
  33      lapply (lt_min_to_false … ltnp ltp)
  34      >(prime_to_primeb_true ? primep) #H destruct (H)
  35     ]
  36   |%{2} %
  37     [%[<Hn @lt_O_S | @primeb_true_to_prime //]
  38     |#p #primep #lt2 @False_ind @(absurd … lt2)
  39      @le_to_not_lt @prime_to_lt_SO //
  40     ]
  41   ]
  42 qed.
  43
  44 lemma not_not_bertrand_to_bertrand1: ∀n.
  45 ¬(not_bertrand n) → ∀x. n ≤ x → x ≤ 2*n →
  46   (∀p.x < p → p ≤ 2*n → ¬(prime p))
  47   → ∃p.n < p ∧ p ≤ x ∧ (prime p).
  48 #n #not_not #x #lenx elim lenx
  49   [#len #Bn @False_ind @(absurd ?? not_not) @Bn
  50   |#n1 #lenn1 #Hind #ltn1 #HB cases (true_or_false (primeb (S n1))) #Hc
  51     [%{(S n1)} % [% [@le_S_S // |//] |@primeb_true_to_prime // ]
  52     |cases (Hind ??)
  53       [#p * * #ltnp #lep #primep %{p} %[%[@ltnp|@le_S//]|//]
  54       |@lt_to_le //
  55       |#p #ltp #lep cases (le_to_or_lt_eq ?? ltp) #Hcase
  56         [@HB // |<Hcase @primeb_false_to_not_prime //]
  57       ]
  58     ]
  59   ]
  60 qed.
  61
  62 theorem not_not_bertrand_to_bertrand: ∀n.
  63   ¬(not_bertrand n) → bertrand n.
  64 #n #not_not @(not_not_bertrand_to_bertrand1 ?? (2*n)) //
  65 #p #le2n #lep @False_ind @(absurd ? le2n) @le_to_not_lt //
  66 qed.
  67
  68 definition k ≝ λn,p.
  69   ∑_{i < log p n}((n/(exp p (S i))\mod 2)).
  70
  71 lemma k_def : ∀n,p. k n p = ∑_{i < log p n}((n/(exp p (S i))\mod 2)).
  72 // qed.
  73
  74 theorem le_k: ∀n,p. k n p ≤ log p n.
  75 #n #p >k_def elim (log p n)
  76   [@le_n
  77   |#n1 #Hind >bigop_Strue
  78     [>(plus_n_O n1) in ⊢ (??%); >plus_n_Sm >commutative_plus
  79      @le_plus
  80       [@Hind
  81       |@le_S_S_to_le @lt_mod_m_m @lt_O_S
  82       ]
  83     |//
  84     ]
  85   ]
  86 qed.
  87
  88 definition Bk ≝ λn.
  89   ∏_{p < S n | primeb p}(exp p (k n p)).
  90
  91 lemma Bk_def : ∀n. Bk n = ∏_{p < S n | primeb p}(exp p (k n p)).
  92 // qed.
  93
  94 definition Dexp ≝ mk_Dop nat 1 timesAC (λa,b.exp b a) ??.
  95   [// | normalize //]
  96 qed.
  97
  98 theorem eq_B_Bk: ∀n. B n = Bk n.
  99 #n >Bdef >Bk_def @same_bigop
 100   [// |#i #ltiS #_ >k_def @exp_sigma_l]
 101 qed.
 102
 103 definition B1 ≝ λn.
 104   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 105
 106 lemma B1_def : ∀n.
 107   B1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 108 // qed.
 109
 110 definition B2 ≝ λn.
 111   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 112
 113 lemma B2_def : ∀n.
 114   B2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 115 // qed.
 116
 117 theorem eq_Bk_B1_B2: ∀n.
 118   Bk n = B1 n * B2 n.
 119 #n >Bk_def >B1_def >B2_def <times_pi
 120 @same_bigop
 121   [//
 122   |#p #ltp #primebp cases (true_or_false (leb (k n p) 1)) #Hc >Hc
 123     [>(lt_to_leb_false 2 (k n p))
 124       [<times_n_1 >commutative_times <times_n_1 //
 125       |@le_S_S @leb_true_to_le //
 126       ]
 127     |>(le_to_leb_true 2 (k n p))
 128       [>commutative_times <times_n_1 >commutative_times <times_n_1 //
 129       |@not_le_to_lt @leb_false_to_not_le //
 130       ]
 131     ]
 132   ]
 133 qed.
 134
 135 lemma lt_div_to_times: ∀n,m,q. O < q → n/q < m → n < q*m.
 136 #n #m #q #posq #ltm
 137 cut (O < m) [@(ltn_to_ltO …  ltm)] #posm
 138 @not_le_to_lt % #len @(absurd …ltm) @le_to_not_lt @le_times_to_le_div //
 139 qed.
 140
 141 (* integrare in div_and_mod *)
 142 lemma lt_to_div_O:∀n,m. n < m → n / m = O.
 143 #n #m #ltnm @(div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 144   [@div_mod_spec_div_mod @(ltn_to_ltO ?? ltnm)
 145   |@div_mod_spec_intro //
 146   ]
 147 qed.
 148
 149 (* the value of n could be smaller *)
 150 lemma k1: ∀n,p. 18 ≤ n → p ≤ n → 2*n/ 3 < p → k (2*n) p = O.
 151 #n #p #le18 #lep #ltp >k_def
 152 elim (log p (2*n))
 153   [//
 154   |#i #Hind >bigop_Strue
 155     [>Hind <plus_n_O cases i
 156       [<exp_n_1
 157        cut (2*n/p = 2) [2:#Hcut >Hcut //]
 158        @lt_to_le_times_to_lt_S_to_div
 159         [@(ltn_to_ltO ?? ltp)
 160         |<commutative_times @monotonic_le_times_r //
 161         |>commutative_times in ⊢ (??%); @lt_div_to_times //
 162         ]
 163       |#n2 cut (2*n/(p)\sup(S (S n2)) = O) [2:#Hcut >Hcut //]
 164        @lt_to_div_O @(le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 165         [@(le_times_to_le (exp 3 2))
 166           [@leb_true_to_le //
 167           |>commutative_times in ⊢ (??%); > times_exp
 168            @(transitive_le ? (exp n 2))
 169             [<associative_times >exp_2 in ⊢ (??%); @le_times [@le18|//]
 170             |@(le_exp1 … (lt_O_S ?))
 171              @(le_plus_to_le 3)
 172              cut (3+2*n/3*3 = S(2*n/3)*3) [//] #eq1 >eq1
 173              @(transitive_le ? (2*n))
 174               [normalize in ⊢(??%); <plus_n_O
 175                @monotonic_le_plus_l @(transitive_le ? 18 … le18)
 176                @leb_true_to_le //
 177               |@lt_to_le @lt_div_S @lt_O_S
 178               ]
 179             ]
 180           ]
 181         |@(lt_to_le_to_lt ? (exp p 2))
 182           [@lt_exp1 [@lt_O_S|//]
 183           |@le_exp [@(ltn_to_ltO ?? ltp) |@le_S_S @le_S_S @le_O_n]
 184           ]
 185         ]
 186       ]
 187     |//
 188     ]
 189   ]
 190 qed.
 191
 192 theorem le_B1_theta:∀n.18 ≤ n → not_bertrand n →
 193   B1 (2*n) ≤ theta (2 * n / 3).
 194 #n #le18 #not_Bn >B1_def >theta_def
 195 @(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 196   [@le_pi #p #ltp #primebp @le_exp
 197     [@prime_to_lt_O @primeb_true_to_prime //
 198     |cases (true_or_false (leb (k (2*n) p) 1)) #Hc
 199       [cases (le_to_or_lt_eq ? ? (leb_true_to_le ?? Hc)) -Hc #Hc
 200         [lapply (le_S_S_to_le ?? Hc) -Hc #Hc
 201          @(le_n_O_elim ? Hc) <times_n_O @le_n
 202         |>(eq_to_eqb_true ?? Hc) >Hc @le_n
 203         ]
 204       |>Hc @le_O_n
 205       ]
 206     ]
 207   |@(transitive_le ? (∏_{p < S (2*n/3) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 208     [>(pad_bigop_nil (S(2*n)) (S (2*n/3)) primeb ? 1 timesA) [//]
 209       [#i #lei #lti whd in not_Bn;
 210        cases (decidable_le (S n) i) #Hc
 211         [%1 @not_prime_to_primeb_false @not_Bn [//|@le_S_S_to_le //]
 212         |%2 >k1 // @not_lt_to_le @Hc
 213         ]
 214       |@le_S_S @le_times_to_le_div2
 215         [@lt_O_S
 216         |>commutative_times in ⊢ (??%); @le_times //
 217         ]
 218       ]
 219     |@le_pi #i #lti #primei cases (eqb (k (2*n) i) 1)
 220       [<exp_n_1 @le_n
 221       |normalize @prime_to_lt_O @primeb_true_to_prime //
 222       ]
 223     ]
 224   ]
 225 qed.
 226
 227 theorem le_B2_exp: ∀n. exp 2 7 ≤ n →
 228   B2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
 229 #n #len >B2_def
 230 cut (O < n) [@(lt_to_le_to_lt … len) @leb_true_to_le //] #posn
 231 @(transitive_le ?
 232    (∏_{p < S (sqrt (2*n)) | primeb p}
 233       (p\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
 234   [>(pad_bigop_nil (S (2*n)) (S(sqrt(2*n))) primeb ? 1 timesA)
 235     [//|3: @le_S_S @le_sqrt_n]
 236    #p #lep #ltp cases (true_or_false (leb 2 (k (2*n) p))) #Hc
 237     [@False_ind @(absurd ?? (lt_to_not_le ?? lep))
 238      @(true_to_le_max … ltp) @le_to_leb_true <exp_2
 239      @not_lt_to_le % #H2n
 240      @(absurd ?? (le_to_not_lt 2 (log p (2*n)) ?))
 241       [@le_S_S @f_false_to_le_max
 242         [%{0} %
 243           [>(times_n_1 0) in ⊢ (?%?); >commutative_times in ⊢ (?%?);
 244            @lt_times //
 245           |@le_to_leb_true @(transitive_le ? n) //
 246           ]
 247         |#m #lt1m @lt_to_leb_false @(lt_to_le_to_lt … H2n)
 248          @le_exp [@(ltn_to_ltO ?? lep) |//]
 249         ]
 250       |@(transitive_le ? (k (2*n) p)) [@leb_true_to_le //|@le_k]
 251       ]
 252     |%2 >Hc %
 253     ]
 254   |@(transitive_le ? (∏_{p < S (sqrt (2*n)) | primeb p} (2*n)))
 255     [@le_pi #p #ltp #primep @(transitive_le ? (exp p (log p (2*n))))
 256       [@le_exp
 257         [@prime_to_lt_O @primeb_true_to_prime //
 258         |cases (true_or_false (leb 2 (k (2*n) p))) #Hc >Hc
 259           [>commutative_times <times_n_1 @le_k|@le_O_n]
 260         ]
 261       |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times //
 262       ]
 263     |@(transitive_le ? (exp (2*n) (prim(sqrt (2*n)))))
 264       [>exp_sigma //
 265       |@le_exp
 266         [>(times_n_O O) in ⊢ (?%?); @lt_times //
 267         |@le_prim_n3 @true_to_le_max
 268           [@(transitive_le ? (2*(exp 2 7)))
 269             [@leb_true_to_le // |@le_S @monotonic_le_times_r //]
 270           |@le_to_leb_true @(transitive_le ? (2*(exp 2 7)))
 271             [@leb_true_to_le % | @monotonic_le_times_r //]
 272           ]
 273         ]
 274       ]
 275     ]
 276   ]
 277 qed.
 278
 279 theorem not_bertrand_to_le_B:
 280   ∀n.exp 2 7 ≤ n → not_bertrand n →
 281   B (2*n) ≤ (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 282 #n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times
 283   [@(transitive_le ? (theta ((2*n)/3)))
 284     [@le_B1_theta [@(transitive_le … len) @leb_true_to_le //|//]
 285     |@le_theta
 286     ]
 287   |@le_B2_exp //
 288   ]
 289 qed.
 290
 291 (*
 292 theorem not_bertrand_to_le1:
 293 \forall n.18 \le n \to not_bertrand n \to
 294 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
 295 *)
 296
 297 lemma le_times_div_m_m: ∀n,m. O < m → n/m*m ≤ n.
 298 #n #m #posm >(div_mod n m) in ⊢ (??%); //
 299 qed.
 300
 301 theorem not_bertrand_to_le1:
 302   ∀n.exp 2 7 ≤ n → not_bertrand n →
 303   exp 2 (2*n / 3) ≤ exp (2*n) (sqrt(2*n)/2).
 304 #n #len #notB @(le_times_to_le (exp 2 (2*(2 * n / 3))))
 305   [@lt_O_exp @lt_O_S
 306   |<exp_plus_times @(transitive_le ? (exp 2 (2*n)))
 307     [@(le_exp … (lt_O_S ?))
 308      cut (2*(2*n/3)+2*n/3 = 3*(2*n/3)) [//] #Heq >Heq
 309      >commutative_times @le_times_div_m_m @lt_O_S
 310     |@(transitive_le ? (2*n*B(2*n)))
 311       [@le_exp_B @(transitive_le …len) @leb_true_to_le //
 312       |<(S_pred (sqrt (2*n)/2))
 313         [whd in ⊢ (??(??%)); <associative_times
 314          <commutative_times in ⊢ (??%); @monotonic_le_times_r
 315          @not_bertrand_to_le_B //
 316         |@(le_times_to_le_div … (lt_O_S ?))
 317          @(transitive_le ? (sqrt (exp 2 8)))
 318           [@leb_true_to_le %
 319           |@monotonic_sqrt >commutative_times @le_times //
 320           ]
 321         ]
 322       ]
 323     ]
 324   ]
 325 qed.
 326
 327 theorem not_bertrand_to_le2:
 328   ∀n.exp 2 7 ≤ n → not_bertrand n →
 329   2*n / 3 ≤ (sqrt(2*n)/2)*S(log 2 (2*n)).
 330 #n #len #notB <(eq_log_exp 2 (2*n/3) (le_n ?))
 331 @(transitive_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
 332   [@le_log [@le_n|@not_bertrand_to_le1 //] |@log_exp1 @le_n]
 333 qed.
 334
 335 lemma lt_div_S_div: ∀n,m. O < m → exp m 2 ≤ n →
 336   n/(S m) < n/m.
 337 #n #m #posm #len @lt_times_to_lt_div @(lt_to_le_to_lt ? (S(n/m)*m))
 338   [@lt_div_S //
 339   |<times_n_Sm >commutative_times <times_n_Sm >commutative_times @le_plus [2://]
 340    @le_times_to_le_div //
 341   ]
 342 qed.
 343
 344 lemma times_div_le: ∀a,b,c,d.O < b → O < d →
 345   (a/b)*(c/d) ≤ (a*c)/(b*d).
 346 #a #b #c #d #posa #posb @le_times_to_le_div
 347   [>(times_n_O O) @lt_times //
 348   |cut (∀n,m,p,q.n*m*(p*q) = p*n*(q*m)) [//] #Heq >Heq
 349    @le_times //
 350   ]
 351 qed.
 352
 353 lemma tech: ∀n. 2*(S(log 2 (2*n))) ≤ sqrt (2*n) →
 354   (sqrt(2*n)/2)*S(log 2 (2*n)) ≤ 2*n / 4.
 355 #n #H
 356 cut (4 = 2*2) [//] #H4
 357 cut (4*(S(log 2 (2*n))) ≤ 2* sqrt(2*n))
 358   [>H4 >associative_times @monotonic_le_times_r @H] #H1
 359 >commutative_times @(le_times_to_le_div … (lt_O_S ?))
 360 <associative_times @(transitive_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
 361   [@le_times [@H1|@le_n]
 362   |@(transitive_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
 363     [@le_times_div_div_times @lt_O_S
 364     |>associative_times >commutative_times >(div_times … (lt_O_S …)) @leq_sqrt_n
 365     ]
 366   ]
 367 qed.
 368
 369 (* we need a "good" lower bound for sqrt (2*n) *)
 370 lemma exp_to_log_r : ∀b,n,m. 1 < b → n < m → exp b n ≤ m → n ≤ log b m.
 371 #b #n #m #lt1b #ltnm #Hexp @true_to_le_max [@ltnm |@le_to_leb_true //]
 372 qed.
 373
 374 lemma square_double :∀n. 2 < n → (S n)*(S n) ≤ 2*n*n.
 375 #n #posn normalize <times_n_Sm <plus_n_O >(plus_n_O (n+(n+n*n)))
 376 cut (S(n+(n+n*n)+0)=n*n+(n+(S n))) [//] #Hcut >Hcut >distributive_times_plus_r
 377 @monotonic_le_plus_r <plus_n_Sm cut (n+n = 2*n) [//] #Hcut1 >Hcut1
 378 @monotonic_lt_times_l [@(ltn_to_ltO … posn) |@posn]
 379 qed.
 380
 381 lemma sqrt_bound: ∀n. exp 2 8 ≤ n → 2*(S(log 2 (2*n))) ≤ sqrt (2*n).
 382 #n #len
 383 cut (8 ≤ log 2 n) [<(eq_log_exp 2 8) [@le_log [@le_n|@len]|@le_n]] #Hlog
 384 cut (0<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
 385 >(exp_n_1 2) in ⊢ (? (? ? (? (? ? (? % ?)))) ?);
 386 >(log_exp … (le_n ?) posn) >commutative_plus >plus_n_Sm @true_to_le_max
 387   [@le_S_S @monotonic_le_times_r
 388    cut (2<n) [@(lt_to_le_to_lt … len) @le_S_S @le_S_S @lt_O_S] #lt2n
 389    elim lt2n [//] #m #lt2m #Hind
 390    cut (0<m) [@(transitive_le … lt2m) @leb_true_to_le //] #posm
 391    @(transitive_le ? (log 2 (2*m) +2))
 392     [@le_plus [2://] @le_log [//] normalize <plus_n_O
 393      >(plus_n_O m) in ⊢ (?%?); >plus_n_Sm @monotonic_le_plus_r //
 394     |>(exp_n_1 2) in ⊢ (?(?(??%)?)?);>(log_exp … (le_n ?) posm) @le_S_S @Hind
 395     ]
 396   |@le_to_leb_true >associative_times @monotonic_le_times_r
 397    >commutative_plus
 398    lapply len @(nat_elim1 n) #m #Hind #lem
 399    cut (8<m) [@(transitive_le … lem) @leb_true_to_le //] #lt8m
 400    cut (1<m) [@(transitive_le … lt8m) @leb_true_to_le //] #lt1m
 401    cut (0<m) [@(transitive_le … lt1m) @leb_true_to_le //] #posm
 402    cases (le_to_or_lt_eq … (le_exp_log 2 m posm)) #Hclog
 403     [@(transitive_le … (le_exp_log 2 m posm))
 404      lapply (Hind … Hclog ?) [@le_exp [@lt_O_S|@exp_to_log_r [@le_n|@lt8m|@lem]]]
 405      -Hind #Hind @(transitive_le … Hind) >(eq_log_exp … (le_n ?)) @le_n
 406     |cases (le_to_or_lt_eq … lem) -lem #Hcasem
 407       [lapply (Hind (2^((log 2 m)-1)) ??)
 408         [@le_exp [@lt_O_S] @le_plus_to_minus_r
 409          @(lt_exp_to_lt 2 8) [@lt_O_S | >Hclog @Hcasem]
 410         |<Hclog in ⊢ (??%); @(lt_exp … (le_n…)) whd >(plus_n_O (log 2 m -1))
 411          >plus_n_Sm <plus_minus_m_m [@le_n | @lt_O_log @lt1m]
 412         |-Hind #Hind lapply (le_times … Hind (le_n 2))
 413          cut (∀a,b. a^(b+1) = a^b*a) [#a #b <plus_n_Sm <plus_n_O //] #exp_S
 414          <exp_S <plus_minus_m_m [2:@lt_O_log //]
 415          -Hind #Hind <Hclog @(transitive_le … Hind)
 416          >(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?))
 417          >plus_minus_associative [2:@lt_O_log //]
 418          cut (2+3 ≤ 2+log 2 m)
 419           [@monotonic_le_plus_r @(le_exp_to_le 2) [@le_n|>Hclog @lt_to_le @lt8m]]
 420          generalize in match (2+log 2 m); #a #Hle >(commutative_times 2 a)
 421          <associative_times @le_times [2://] <associative_times
 422          >(commutative_times ? 2) lapply Hle cases a
 423           [//| #a0 -Hle #Hle whd in match (S a0 -1); <(minus_n_O a0)
 424            @square_double @le_S_S_to_le @lt_to_le @Hle]
 425         ]
 426       |<Hcasem >(eq_log_exp … (le_n ?)) @leb_true_to_le %
 427       ]
 428     ]
 429   ]
 430 qed.
 431
 432 theorem bertrand_up:
 433    ∀n. 2^8 ≤ n → bertrand n.
 434 #n #len @not_not_bertrand_to_bertrand % #notBn
 435 @(absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))))
 436   [@not_bertrand_to_le2
 437     [@(transitive_le ???? len) @le_exp [@lt_O_S|@le_n_Sn]|//]
 438   |@lt_to_not_le
 439    @(le_to_lt_to_lt ???? (lt_div_S_div ????))
 440     [@tech @sqrt_bound //
 441     |@(transitive_le ? (2*exp 2 8))
 442       [@leb_true_to_le // |@monotonic_le_times_r //]
 443     |@lt_O_S
 444     ]
 445   ]
 446 qed.
 447
 448 (* see Bertrand256 for the complete theorem *)
 449