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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/neper.ma".
  16
  17 definition C \def \lambda n.pi_p (S n) primeb
  18   (\lambda p.match (leb (p*p) n) with
  19     [ true => p
  20     | false => S (n/p) ]).
  21
  22 theorem asdasd : \forall n. exp n (prim n) \leq (A n)*(C n).
  23 intro;unfold prim;rewrite < exp_sigma_p;unfold A;unfold C;rewrite < times_pi_p;
  24 apply le_pi_p;intros;
  25 apply (bool_elim ? (leb (i*i) n));intro
  26     [change in \vdash (? ? (? ? %)) with i;
  27      rewrite > sym_times;change in \vdash (? ? %) with (exp i (S (log i n)));
  28      apply lt_to_le;apply lt_exp_log;apply prime_to_lt_SO;
  29      apply primeb_true_to_prime;assumption
  30     |change in \vdash (? ? (? ? %)) with (S (n/i));
  31      cut (log i n = S O)
  32        [rewrite > Hcut;rewrite < exp_n_SO;
  33         apply lt_to_le;rewrite > sym_times;apply lt_div_S;apply prime_to_lt_O;
  34         apply primeb_true_to_prime;assumption
  35        |apply antisymmetric_le
  36          [apply le_S_S_to_le;apply not_le_to_lt;intro;
  37           apply (leb_false_to_not_le ? ? H2);apply (trans_le ? (exp i (log i n)))
  38            [rewrite < exp_SSO;apply le_exp;
  39               [apply prime_to_lt_O;
  40                apply primeb_true_to_prime;assumption
  41               |assumption]
  42            |apply le_exp_log;apply (trans_le ? i)
  43               [apply prime_to_lt_O;apply primeb_true_to_prime;assumption
  44               |apply le_S_S_to_le;assumption]]
  45          |apply (trans_le ? (log i i))
  46            [rewrite > log_n_n;
  47               [apply le_n
  48               |apply prime_to_lt_SO;apply primeb_true_to_prime;assumption]
  49            |apply le_log
  50               [apply prime_to_lt_SO;apply primeb_true_to_prime;assumption
  51               |apply le_S_S_to_le;assumption]]]]]
  52 qed.
  53
  54 definition theta_pi \def
  55   \lambda n.pi_p (S n) primeb (\lambda p.p).
  56
  57 definition C1 \def
  58   \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (x*x) n)) (\lambda p.p).
  59
  60 definition C2 \def
  61   \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (S n) (x*x))) (\lambda p.S (n/p)).
  62
  63
  64 theorem jj : \forall n.C n = C1 n * C2 n.
  65 intro;unfold C;unfold C1;unfold C2;
  66 cut (\forall m.pi_p (S n) primeb
  67 (λp:nat
  68  .match leb (p*p) m in bool return λb:bool.nat with
  69   [true⇒p|false⇒S (m/p)])
  70 =pi_p (S n) (λx:nat.primeb x∧leb (x*x) m) (λp:nat.p)
  71  *pi_p (S n) (λx:nat.primeb x∧leb (S m) (x*x)) (λp:nat.S (m/p)))
  72   [apply Hcut;
  73   |intro;elim n 0
  74      [simplify;reflexivity
  75      |intro;apply (bool_elim ? (primeb (S n1)))
  76         [intros;rewrite > true_to_pi_p_Sn
  77            [apply (bool_elim ? (leb ((S n1)*(S n1)) m))
  78               [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
  79                  [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
  80                     [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
  81                     |rewrite > H;lapply (leb_true_to_le ? ? H2);
  82                      lapply (le_to_not_lt ? ? Hletin);
  83                      apply (bool_elim ? (leb (S m) (S n1 * S n1)))
  84                        [intro;apply False_ind;apply Hletin1;
  85                         apply leb_true_to_le;assumption
  86                        |intro;reflexivity]]
  87                  |rewrite > H2;rewrite > H;reflexivity]
  88               |intro;rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
  89                  [rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? ? %))
  90                     [rewrite > H1;rewrite < assoc_times;
  91                      rewrite > sym_times in \vdash (? ? (? % ?) ?);
  92                      rewrite > assoc_times;reflexivity
  93                     |rewrite > H;
  94                      change in \vdash (? ? % ?) with (leb (S m) (S n1* S n1));
  95                      apply le_to_leb_true;apply not_le_to_lt;
  96                      apply leb_false_to_not_le;assumption]
  97                  |rewrite > H;rewrite > H2;reflexivity]]
  98            |assumption]
  99         |intros;rewrite > false_to_pi_p_Sn
 100            [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
 101               [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
 102                  [rewrite > H1;reflexivity
 103                  |rewrite > H;elim (leb (S m) (S n1*S n1));simplify;reflexivity]
 104               |rewrite > H;elim (leb (S n1*S n1) m);simplify;reflexivity]
 105            |assumption]]]]
 106 qed.
 107
 108 theorem log_pi_p : \forall n,b,f,g.S O < b \to
 109   log b (pi_p n f g) \leq
 110     (sigma_p n f (\lambda x.S O)) + (sigma_p n f (\lambda x.log b (g x))).
 111 intros;elim n
 112   [simplify;rewrite < times_n_SO;apply (leb_elim b (S O))
 113     [intro;elim (lt_to_not_le ? ? H);assumption
 114     |intro;simplify;apply le_n]
 115   |apply (bool_elim ? (f n1))
 116     [intro;rewrite > true_to_pi_p_Sn
 117        [rewrite > true_to_sigma_p_Sn
 118           [rewrite > true_to_sigma_p_Sn
 119              [apply (trans_le ? (S ((log b (g n1)) + (log b (pi_p n1 f g)))))
 120                 [apply log_times;assumption
 121                 |rewrite > assoc_plus;
 122                  change in \vdash (? ? %) with (S (sigma_p n1 f (\lambda x.S O)+(log b (g n1)+sigma_p n1 f (\lambda x.log b (g x)))));
 123                  apply le_S_S;rewrite < assoc_plus;
 124                  rewrite > sym_plus in \vdash (? ? (? % ?));
 125                  rewrite > assoc_plus;apply le_plus;
 126                    [apply le_n]]]]]
 127      assumption
 128     |intro;rewrite > false_to_pi_p_Sn
 129        [rewrite > false_to_sigma_p_Sn
 130           [rewrite > false_to_sigma_p_Sn]]
 131      assumption]]
 132 qed.
 133
 134 axiom daemon : False.
 135 (*
 136 lemma lt_log_to_lt : \forall b,m,n.S O < b \to log b m < log b n \to m < n.
 137 intros;apply not_le_to_lt;intro;elim (le_to_not_lt ? ? (le_log ? ? ? H H2));
 138 assumption.
 139 qed.
 140
 141 theorem ababbs: \forall n,a,b.S O < b \to O < n \to n < exp b a \to log b n < a.
 142 intros;unfold log;apply not_le_to_lt;intro;apply (lt_to_not_le ? ? H2);
 143 elim (le_to_or_lt_eq ? ? H3)
 144   [apply lt_to_le;apply (lt_log_to_lt b ? ? H);rewrite > eq_log_exp;assumption
 145   |apply (trans_le ? (exp b (log b n)))
 146      [rewrite < H4;apply le_n
 147      |apply le_exp_log;assumption]]
 148 qed.
 149
 150 theorem exp_exp_to_log : \forall b,n,k.S O < b \to
 151 exp b k \leq n \to n < exp b (S k) \to log b n = k.
 152 intros;unfold log;lapply (ababbs ? ? ? H ? H2)
 153   [apply (trans_le ? ? ? ? H1);apply lt_O_exp
 154   |unfold log in Hletin;lapply (le_to_leb_true ? ? H1);
 155    lapply (f_m_to_le_max (λx:nat.leb ((b)\sup(x)) n) n ? ? Hletin1)
 156      [
 157   elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? Hletin))
 158      [unfold log in H3;
 159 ]]elim daemon.
 160 qed.
 161
 162 theorem xxx_log : \forall a,b.S O < b \to O < a \to log b (b*a) = S (log b a).
 163 intros 3;elim a
 164   [elim (not_le_Sn_O ? H1);
 165   |apply (inj_exp_r b)
 166      [assumption
 167      |*)
 168
 169 theorem le_log_C2_sigma_p : \forall n,b. S O < b \to
 170 log b (C2 n) \leq
 171 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
 172 (prim n + (((sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i.prim i * S (n!/i)))
 173   *(S (log b 3)))/n!)).
 174 intros;unfold C2;
 175 apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1)
 176 +sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x))
 177  (λi.log b (S (n/i)))))
 178   [apply log_pi_p;assumption
 179   |apply le_plus
 180      [apply le_n
 181      |apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λi:nat.S (log b (n/i)))))
 182         [apply le_sigma_p;intros;cut (log b (b*(n/i)) = S (log b (n/i)))
 183            [rewrite < Hcut;apply le_log
 184               [assumption
 185               |elim H
 186                  [rewrite < times_SSO_n;change in \vdash (? % ?) with (S O + (n/i));
 187                   apply le_plus;
 188                     [apply le_times_to_le_div
 189                        [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
 190                        |rewrite < times_n_SO;apply le_S_S_to_le;assumption]
 191                     |apply le_n]
 192                  |apply (trans_le ? ? ? H4);apply le_times_l;apply le_S;apply le_n]]
 193            |rewrite > exp_n_SO in ⊢ (? ? (? ? (? % ?)) ?);
 194             rewrite > log_exp;
 195               [reflexivity
 196               |assumption
 197               |apply le_times_to_le_div;
 198                  [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
 199                  |rewrite < times_n_SO;apply le_S_S_to_le;assumption]]]
 200         |change in ⊢ (? (? ? ? (λi:?.%)) ?) with ((S O) + (log b (n/i)));
 201          rewrite > (sigma_p_plus_1 ? (\lambda x.S O));
 202          apply le_plus
 203            [unfold prim;apply le_sigma_p1;intros;elim (leb (S n) (i*i));
 204               [rewrite > andb_sym;apply le_n
 205               |rewrite > andb_sym;apply le_O_n]
 206            |apply sigma_p_log_div;assumption]]]]
 207 qed.
 208
 209 lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
 210 prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
 211               ((S (S (S (S O))))*n)))/(log b n).
 212 (* la stima del secondo addendo è ottenuta considerando che
 213    logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *)
 214 intros;apply le_times_to_le_div;
 215   [apply lt_O_log;
 216      [apply (trans_le ? b)
 217         [apply lt_to_le;assumption
 218         |assumption]
 219      |assumption]
 220   |apply (trans_le ? (log b (exp n (prim n))))
 221      [rewrite > sym_times;apply log_exp2
 222         [assumption
 223         |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption]
 224      |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O)))))
 225                                *(exp (S (S O)) ((S (S (S (S O))))*n)))))
 226         [apply le_log
 227            [assumption
 228            |apply le_exp_primr;apply (trans_le ? ? ? H H1)]
 229         |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) +
 230                               (log b (exp (S (S O)) ((S (S (S (S O))))*n))))))
 231            [apply log_times;assumption
 232            |apply le_S_S;apply le_plus
 233               [apply log_exp1;assumption
 234               |cases H
 235                  [rewrite > times_n_SO in \vdash (? (? ? %) ?);
 236                   rewrite > log_exp
 237                     [rewrite < plus_n_O;apply le_n
 238                     |apply le_n
 239                     |apply le_n]
 240                  |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O))))))
 241                     [apply log_exp1;apply le_S;assumption
 242                     |rewrite > times_n_SO in \vdash (? ? %);
 243                      apply le_times_r;apply le_S_S;
 244                      rewrite > lt_to_log_O
 245                        [apply le_n
 246                        |apply lt_O_S
 247                        |apply le_S_S;assumption]]]]]]]]
 248 qed.
 249
 250 theorem le_log_C2_stima : \forall n,b. S O < b \to b*b < n \to
 251 log b (C2 n) \leq
 252 (*(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +*)
 253 ((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 254               ((S (S (S (S O))))*n)))/(log b n)) +
 255 (((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 256               ((S (S (S (S O))))*n)))/(log b n)) +
 257  (((sigma_p n (\lambda x.leb (S n) (x*x))
 258               (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
 259               ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
 260   *(S (log b (S (S (S O))))))/n!)).intros.
 261 apply (trans_le ? ? ? (le_log_C2_sigma_p ? ? ?))
 262   [assumption
 263   |apply le_plus
 264      [apply (trans_le ? ? ? ? (le_prim_n_stima ? ? ? ?));
 265       [unfold prim;apply le_sigma_p1;intros;
 266        do 2 rewrite < times_n_SO;elim (primeb i)
 267         [elim (leb (S n) (i*i));simplify [apply le_n|apply le_O_n]
 268         |simplify;apply le_n]
 269       |assumption
 270       |apply (trans_le ? ? ? ? H1);apply le_S;apply le_times_n;
 271        apply lt_to_le;assumption]
 272    |apply le_plus
 273      [apply le_prim_n_stima;
 274        [assumption
 275        |apply (trans_le ? (b*b))
 276           [apply le_times_n;apply lt_to_le;assumption
 277           |apply lt_to_le;assumption]]
 278      |apply monotonic_div
 279         [apply lt_O_fact
 280         |apply le_times_l;apply le_sigma_p;intros;apply le_times_l;
 281          apply le_prim_n_stima
 282            [assumption
 283            |apply (le_exp_to_le1 ? ? (S (S O)));
 284               [apply le_S;apply le_n
 285               |do 2 rewrite > exp_SSO;apply (trans_le ? n)
 286                  [apply lt_to_le;assumption
 287                  |apply lt_to_le;apply leb_true_to_le;assumption]]]]]]]
 288 qed.
 289
 290 lemma log_interval : \forall b,k,n. S O < b \to exp b k \leq n \to n < exp b (S k) \to
 291                        log b n = k.
 292 intros 2.elim k
 293   [simplify in H2;rewrite < times_n_SO in H2;apply lt_to_log_O;assumption
 294   |cut (log b n1 < S (S n))
 295      [cut (n < log b n1)
 296         [apply antisymmetric_le
 297            [apply le_S_S_to_le;assumption
 298            |assumption]
 299         |apply (trans_le ? (log b (exp b (S n))))
 300            [rewrite > eq_log_exp
 301               [apply le_n
 302               |assumption]
 303            |apply le_log;assumption]]
 304      |apply le_S_S;apply (trans_le ? (log b (pred (exp b (S (S n))))))
 305         [apply le_log
 306            [assumption
 307            |apply le_S_S_to_le;apply (trans_le ? ? ? H3);
 308             rewrite > minus_n_O in \vdash (? ? (? (? %)));
 309             rewrite < (eq_minus_S_pred (exp b (S (S n))) O);
 310             rewrite > minus_n_O in \vdash (? % ?);
 311             apply minus_le_S_minus_S]
 312         |unfold log;apply f_false_to_le_max;
 313            [apply (ex_intro ? ? (S n));split
 314               [apply (trans_le ? (exp b (S n)));
 315                  [apply lt_to_le;apply lt_m_exp_nm;assumption
 316                  |rewrite > minus_n_O in ⊢ (? ? (? %));
 317                   rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
 318                   rewrite > sym_plus;
 319                   change in \vdash (? % ?) with (S (O + exp b (S n)));
 320                   apply lt_minus_to_plus;
 321                   change in ⊢ (? ? (? % ?)) with (b * (exp b (S n)));
 322                   rewrite > times_n_SO in \vdash (? ? (? ? %));
 323                   rewrite > sym_times in \vdash (? ? (? % ?));
 324                   rewrite < distributive_times_minus;unfold lt;
 325                   rewrite > times_n_SO in \vdash (? % ?);apply le_times
 326                     [apply lt_O_exp;apply (trans_le ? ? ? ? H1);
 327                      apply le_S;apply le_n
 328                     |apply le_plus_to_minus_r;simplify;assumption]]
 329               |apply le_to_leb_true;
 330                rewrite > minus_n_O in \vdash (? ? (? %));
 331                rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
 332                rewrite > sym_plus;change in \vdash (? % ?) with (S (exp b (S n)));
 333                apply lt_exp;
 334                  [assumption
 335                  |apply le_n]]
 336            |intros;apply lt_to_leb_false;unfold lt;
 337             rewrite > minus_n_O in \vdash (? (? (? %)) ?);
 338             rewrite < eq_minus_S_pred;rewrite < minus_Sn_m
 339               [rewrite > minus_S_S;rewrite < minus_n_O;apply le_exp;
 340                  [apply (trans_le ? ? ? ? H1);apply le_S;apply le_n
 341                  |assumption]
 342               |apply lt_O_exp;apply (trans_le ? ? ? ? H1);apply le_S;apply le_n]]]]]
 343 qed.
 344
 345 lemma log_strano : \forall b,i.S O < b \to S O < i \to
 346                   ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
 347                   (S (S (S O)))*i.
 348 alias num (instance 0) = "natural number".
 349 cut (\forall b,i,k.S O < b \to S O < i \to
 350             (exp b k) \leq i-1 \to i-1 < (exp b (S k)) \to
 351                   ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
 352                   (S (S (S O)))*i)
 353   [intros;apply (Hcut ? ? (log b (i-1)) H H1);
 354      [apply le_exp_log;rewrite > (minus_n_n 1) in \vdash (? % ?);
 355       apply lt_plus_to_lt_minus;
 356         [apply le_n
 357         |rewrite < eq_minus_plus_plus_minus
 358            [rewrite > sym_plus;rewrite > eq_minus_plus_plus_minus;
 359               [rewrite < minus_n_n;rewrite < plus_n_O;assumption
 360               |apply le_n]
 361            |apply lt_to_le;assumption]]
 362      |apply lt_exp_log;assumption]
 363   |intros;rewrite > minus_n_O in ⊢ (? (? (? ? (? ? (? %))) ?) ?);
 364    rewrite < eq_minus_S_pred;rewrite > (log_interval ? k)
 365      [apply (trans_le ? (3*(exp b k) + 3))
 366         [change in \vdash (? (? ? %) ?) with (2+3);
 367          rewrite < assoc_plus;apply le_plus_l;
 368          elim k
 369            [simplify;apply le_S;apply le_n
 370            |elim (decidable_eq_nat O n)
 371               [rewrite < H5;apply (trans_le ? (3*(exp 2 1)));
 372                  [simplify;apply le_n
 373                  |apply le_times_r;apply monotonic_exp1;assumption]
 374               |rewrite < times_n_Sm;apply (trans_le ? (3*(exp b n) + 4))
 375                  [rewrite > assoc_plus;rewrite > sym_plus;apply le_plus_l;
 376                   assumption
 377                  |rewrite < sym_plus;change in \vdash (? % ?) with (S (3 + (3*(exp b n))));
 378                   apply lt_minus_to_plus;
 379                   change in ⊢ (? ? (? (? ? %) ?)) with (b*(exp b n));
 380                   rewrite > sym_times in \vdash (? ? (? (? ? %) ?));
 381                   rewrite < assoc_times;
 382                   rewrite > times_n_SO in ⊢ (? ? (? ? (? ? %)));
 383                   rewrite < assoc_times;rewrite < distr_times_minus;
 384                   apply (trans_le ? (3*2*1))
 385                     [simplify;apply le_S;apply le_S;apply le_n
 386                     |apply le_times
 387                        [apply le_times_r;apply (trans_le ? (exp 2 n))
 388                           [rewrite > exp_n_SO in \vdash (? % ?);apply le_exp
 389                              [apply le_S;apply le_n
 390                              |generalize in match H5;cases n
 391                                 [intro;elim H6;reflexivity
 392                                 |intro;apply le_S_S;apply le_O_n]]
 393                           |apply monotonic_exp1;assumption]
 394                        |apply le_S_S_to_le;rewrite < minus_Sn_m;
 395                           [simplify;rewrite < minus_n_O;assumption
 396                           |apply lt_to_le;assumption]]]]]]
 397         |rewrite > times_n_SO in \vdash (? (? ? %) ?);
 398          rewrite < distr_times_plus;apply le_times_r;
 399          rewrite < plus_n_SO;apply (trans_le ? (S (i-1)))
 400            [apply le_S_S;assumption
 401            |rewrite < minus_Sn_m
 402               [simplify;rewrite < minus_n_O;apply le_n
 403               |apply lt_to_le;assumption]]]
 404      |assumption
 405      |assumption
 406      |assumption]]
 407 qed.
 408
 409 lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
 410 intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
 411   [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
 412    rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
 413    rewrite > div_plus_times
 414      [reflexivity
 415      |generalize in match H;cases z;intros
 416         [elim (not_le_Sn_O ? H2)
 417         |apply lt_times_r;apply lt_mod_m_m;assumption]]
 418   |assumption]
 419 qed.
 420
 421 alias num (instance 0) = "natural number".
 422 lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
 423             (sigma_p n (\lambda x.leb (S n) (x*x))
 424               (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
 425               ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
 426             \leq ((28 * n * n!)/(pred (log b n))).
 427 intros.apply (trans_le ? (sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i. ((7*i)/(log b i))*(S (n!/i)))))
 428   [apply le_sigma_p;intros;cut (b \leq i)
 429      [cut (1 < i) [|apply (trans_le ? ? ? H Hcut)]
 430       apply le_times_l;apply monotonic_div
 431         [apply lt_O_log
 432            [generalize in match H3;cases i
 433               [simplify;intros;destruct H4
 434               |intro;apply le_S_S;apply le_O_n]
 435            |assumption]
 436         |rewrite > sym_times;simplify in ⊢ (? (? (? % ?)) ?);
 437          change in ⊢ (? % ?) with (1 + ((4 + (log b (pred i) * 4)) + 4*i));
 438          rewrite > assoc_plus;rewrite < assoc_plus;
 439          simplify in \vdash (? (? % ?) ?);rewrite < assoc_plus;
 440          apply (trans_le ? (3*i + 4*i))
 441            [apply le_minus_to_plus;rewrite > eq_minus_plus_plus_minus
 442               [rewrite < minus_n_n;rewrite < plus_n_O;
 443                rewrite > sym_plus;rewrite > sym_times;apply log_strano
 444                  [assumption
 445                  |lapply (leb_true_to_le ? ? H3);apply (trans_le ? ? ? H);
 446                   apply (le_exp_to_le1 ? ? 2);
 447                     [apply le_S_S;apply le_O_n
 448                     |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 449                      apply lt_to_le;assumption]]
 450               |apply le_n]
 451            |rewrite > sym_times in \vdash (? (? % ?) ?);
 452             rewrite > sym_times in \vdash (? (? ? %) ?);
 453             rewrite < distr_times_plus;rewrite > sym_times;apply le_n]]
 454      |apply (le_exp_to_le1 ? ? 2);
 455         [apply le_S_S;apply le_O_n
 456         |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 457          apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
 458          apply le_n]]
 459   |apply (trans_le ? (sigma_p n (λx:nat.leb (S n) (x*x)) (λi:nat.7*i/log b i*((2*(n!))/i))))
 460      [apply le_sigma_p;intros;apply le_times_r;apply (trans_le ? (n!/i + n!/i))
 461         [change in \vdash (? % ?) with (1 + n!/i);apply le_plus_l;
 462          apply le_times_to_le_div
 463            [generalize in match H3;cases i;simplify;intro
 464               [destruct H4
 465               |apply le_S_S;apply le_O_n]
 466            |generalize in match H2;cases n;intro
 467               [elim (not_le_Sn_O ? H4)
 468               |change in \vdash (? ? %) with ((S n1)*(n1!));apply le_times
 469                  [apply lt_to_le;assumption
 470                  |apply lt_O_fact]]]
 471         |rewrite > plus_n_O in \vdash (? (? ? %) ?);
 472          change in \vdash (? % ?) with (2 * (n!/i));
 473          apply le_times_div_div_times;
 474          generalize in match H3;cases i;simplify;intro
 475            [destruct H4
 476            |apply le_S_S;apply le_O_n]]
 477      |apply (trans_le ? (sigma_p n (\lambda x:nat.leb (S n) (x*x)) (\lambda i.((14*(n!))/log b i))))
 478         [apply le_sigma_p;intros;
 479          cut (b \leq i)
 480            [|apply (le_exp_to_le1 ? ? 2);
 481               [apply le_S_S;apply le_O_n
 482               |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 483                apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
 484                apply le_n]]
 485          cut (1 < i)
 486            [|apply (trans_le ? ? ? H Hcut)]
 487          change in ⊢ (? ? (? % ?)) with ((7*2)*(n!));
 488          rewrite > assoc_times in \vdash (? ? (? % ?));
 489          apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?));
 490            [apply lt_to_le;assumption
 491            |rewrite > (eq_div_div_times ? ? 7)
 492               [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
 493                rewrite < assoc_times in \vdash (? (? % ?) ?);
 494                apply (trans_le ? ? ? (le_div_times_m ? ? ? ? ?))
 495                  [apply lt_O_log
 496                     [apply lt_to_le;assumption
 497                     |assumption]
 498                  |unfold lt;rewrite > times_n_SO in \vdash (? % ?);
 499                   apply le_times;
 500                     [apply le_S_S;apply le_O_n
 501                     |apply lt_to_le;assumption]
 502                  |apply le_n]
 503               |apply le_S_S;apply le_O_n
 504               |apply lt_to_le;assumption]]
 505         |apply (trans_le ? (sigma_p (S n) (\lambda x.leb (S n) (x*x))
 506                       (\lambda i.14*n!/log b i)))
 507            [apply (bool_elim ? (leb (S n) (n*n)));intro
 508               [rewrite > true_to_sigma_p_Sn
 509                  [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
 510                   apply le_plus_r;apply le_O_n
 511                  |assumption]
 512               |rewrite > false_to_sigma_p_Sn
 513                  [apply le_n
 514                  |assumption]]
 515            |apply (trans_le ? ? ? (le_sigma_p_div_log_div_pred_log ? ? ? ? ?));
 516               [assumption
 517               |apply lt_to_le;assumption
 518               |rewrite < assoc_times;
 519                rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?);
 520                rewrite < assoc_times;apply le_n]]]]]
 521 qed.
 522
 523 theorem le_log_C2_stima2 : \forall n,b. S O < b \to b*b < n \to
 524 log b (C2 n) \leq
 525 (14*n/(log b n)) +
 526  ((((28*n*n!)/pred (log b n))
 527   *(S (log b (S (S (S O))))))/n!).intros.
 528 apply (trans_le ? ? ? (le_log_C2_stima ? ? H H1));
 529 rewrite < assoc_plus in \vdash (? % ?);apply le_plus
 530   [rewrite > times_SSO_n in \vdash (? % ?);
 531    apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?))
 532      [apply lt_O_log
 533        [apply (trans_le ? (b*b))
 534           [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
 535           |apply lt_to_le;assumption]
 536        |apply (trans_le ? (b*b))
 537           [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 538              [apply le_n|apply lt_to_le;assumption]
 539           |apply lt_to_le;assumption]]
 540      |change in \vdash (? ? (? (? % ?) ?)) with (2*7);
 541       apply monotonic_div;
 542         [apply lt_O_log
 543           [apply (trans_le ? (b*b))
 544              [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
 545              |apply lt_to_le;assumption]
 546           |apply (trans_le ? (b*b))
 547              [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 548                 [apply le_n|apply lt_to_le;assumption]
 549              |apply lt_to_le;assumption]]
 550         |rewrite > assoc_times;apply le_times_r;
 551          change in \vdash (? (? (? (? ? %) ?)) ?) with (1 + (log b (pred n)));
 552          rewrite > distr_times_plus;
 553          change in \vdash (? % ?) with (1 + (4*1+4*log b (pred n)+4*n));
 554          do 2 rewrite < assoc_plus;simplify in ⊢ (? (? (? % ?) ?) ?);
 555          change in ⊢ (? ? %) with ((3+4)*n);rewrite > sym_times in \vdash (? ? %);
 556          rewrite > distr_times_plus;
 557          rewrite > sym_times in \vdash (? ? (? % ?));
 558          rewrite > sym_times in \vdash (? ? (? ? %));
 559          apply le_plus_l;rewrite > sym_plus;apply log_strano
 560            [assumption
 561            |apply (trans_le ? ? ? H);apply (trans_le ? (b*b))
 562               [rewrite > times_n_SO in \vdash (? % ?);
 563                apply le_times_r;apply lt_to_le;assumption
 564               |apply lt_to_le;assumption]]]]
 565   |apply monotonic_div
 566      [apply lt_O_fact
 567      |apply le_times_l;apply (le_sigma_p_lemma1 ? ? H H1)]]
 568 qed.
 569
 570 theorem le_log_C2_stima3 : \forall n,b. S O < b \to b*b < n \to
 571 log b (C2 n) \leq
 572 (14*n/(log b n)) +
 573  ((28*n)*(S (log b (S (S (S O)))))/pred (log b n)).intros.
 574 apply (trans_le ? ? ? (le_log_C2_stima2 ? ? H H1));apply le_plus_r;
 575 (*apply (trans_le ? ((28*n)*(28*n*n!/pred (log b n)*S (log b 3)/(28*n*n!))))
 576   [*)
 577 rewrite > (eq_div_div_times ? ? (28*n)) in \vdash (? % ?)
 578   [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
 579    rewrite < assoc_times;
 580    apply le_div_times_m;
 581      [apply (trans_le ? (pred (log b (b*b))))
 582         [rewrite < exp_SSO;rewrite > eq_log_exp;
 583            [apply le_n
 584            |assumption]
 585         |rewrite < exp_SSO;rewrite > eq_log_exp;
 586            [simplify;rewrite > minus_n_O in \vdash (? ? (? %));
 587             rewrite < eq_minus_S_pred;
 588             apply le_plus_to_minus_r;simplify;
 589             rewrite < (eq_log_exp b 2);
 590               [apply le_log
 591                  [assumption
 592                  |rewrite > exp_SSO;apply lt_to_le;assumption]
 593               |assumption]
 594            |assumption]]
 595      |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
 596         [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 597            [apply le_S_S;apply le_O_n
 598            |apply (trans_le ? ? ? ? H1);apply le_S_S;
 599             rewrite > times_n_SO;apply le_times
 600               [apply le_O_n
 601               |apply lt_to_le;assumption]]
 602         |apply lt_O_fact]]
 603   |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
 604      [apply le_S_S;apply le_O_n
 605      |apply (trans_le ? ? ? ? H1);apply le_S_S;
 606       rewrite > times_n_SO;apply le_times
 607         [apply le_O_n
 608         |apply lt_to_le;assumption]]
 609   |apply lt_O_fact]
 610 qed.
 611
 612 lemma le_prim_log1: \forall n,b. S O < b \to O < n \to
 613                      (prim n)*(log b n) \leq
 614                      log b (A n) + log b (C1 n) + log b (C2 n) + 2.
 615 intros.change in \vdash (? ? (? ? %)) with (1+1).
 616 rewrite < assoc_plus;rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)).
 617 rewrite > assoc_plus in ⊢ (? ? (? % ?));
 618 apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1));
 619   [apply (trans_le ? (log b (A n * (C1 n * C2 n))))
 620      [apply (trans_le ? (log b (exp n (prim n))))
 621         [apply log_exp2;assumption
 622         |apply le_log
 623            [assumption
 624            |rewrite < jj;apply asdasd]]
 625      |rewrite > sym_plus;simplify;apply log_times;assumption]
 626   |apply le_plus_l;apply le_plus_r;rewrite > sym_plus;simplify;apply log_times;
 627    assumption]
 628 qed.
 629
 630 lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to
 631                   log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1.
 632 intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n))))))
 633   [apply le_log
 634      [assumption
 635      |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption]
 636   |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n)))))));
 637      [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n)))));
 638       apply log_times;assumption
 639      |apply le_plus_r;apply le_plus;apply log_exp1;assumption]]
 640 qed.
 641
 642 lemma le_theta_pi_A : \forall n.theta_pi n \leq A n.
 643 intro.unfold theta_pi.unfold A.apply le_pi_p.intros.
 644 rewrite > exp_n_SO in \vdash (? % ?).
 645 cut (O < i)
 646   [apply le_exp
 647      [assumption
 648      |apply lt_O_log
 649         [apply (trans_le ? ? ? Hcut);apply le_S_S_to_le;assumption
 650         |apply le_S_S_to_le;assumption]]
 651   |apply prime_to_lt_O;apply primeb_true_to_prime;assumption]
 652 qed.
 653
 654 definition sqrt \def
 655   \lambda n.max n (\lambda x.leb (x*x) n).
 656
 657 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
 658 intros;apply (trans_le ? (sqrt m * sqrt m))
 659   [apply le_times;assumption
 660   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
 661    apply (ex_intro ? ? O);split
 662      [apply le_O_n
 663      |simplify;reflexivity]]
 664 qed.
 665
 666 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
 667 intros;apply (trans_le ? (sqrt m * sqrt m))
 668   [apply (trans_le ? (S n * S n))
 669      [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
 670         [apply le_times_r;apply le_S;apply le_n
 671         |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
 672          apply le_plus_r;apply le_O_n]
 673      |apply le_times;assumption]
 674   |apply le_sqrt_to_le_times_l;apply le_n]
 675 qed.
 676
 677 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
 678 intros;apply not_le_to_lt;intro;
 679 apply ((leb_false_to_not_le ? ?
 680            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
 681          H1);
 682 apply (trans_le ? ? ? ? H1);cases n
 683   [apply le_n
 684   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
 685      [apply le_S_S;apply le_O_n
 686      |apply le_n]]
 687 qed.
 688
 689 theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n.
 690 intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n))
 691   [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n)
 692      [simplify;reflexivity
 693      |apply (bool_elim ? (primeb (S n1)))
 694         [intro;rewrite > true_to_pi_p_Sn
 695            [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %)
 696               [apply eq_f2
 697                  [reflexivity
 698                  |apply H;intros;apply H1;apply le_S;assumption]
 699               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 700                rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n]
 701            |assumption]
 702         |intro;rewrite > false_to_pi_p_Sn
 703            [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %)
 704               [apply H;intros;apply H1;apply le_S;assumption
 705               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 706                rewrite > H2;whd;reflexivity]
 707            |assumption]]]
 708   |apply le_S_S;unfold sqrt;apply le_max_n
 709   |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify
 710      [rewrite > lt_to_leb_false
 711         [reflexivity
 712         |apply le_sqrt_to_le_times_r;assumption]
 713      |reflexivity]]
 714 qed.
 715
 716 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
 717 intro.unfold sqrt.apply le_max_n.
 718 qed.
 719
 720 lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to
 721                      (prim n)*(log b n) \leq
 722                       2*S (log b (pred n))+2*(pred n)*S (log b 2)
 723                       +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 724                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
 725                       +4.
 726 intros.cut (1 < n)
 727   [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) +
 728                      (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) +
 729                      ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2))
 730     [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?))
 731        [apply lt_to_le;assumption
 732        |apply le_plus_l;apply le_plus
 733           [apply le_plus
 734              [apply le_log_A1;assumption
 735              |rewrite < eq_theta_pi_sqrt_C1;apply (trans_le ? (log b (A (sqrt n))))
 736                 [apply le_log
 737                    [assumption
 738                    |apply le_theta_pi_A]
 739                 |apply le_log_A1
 740                    [assumption
 741                    |apply (trans_le ? ? ? H);apply lt_to_le;assumption]]]
 742           |apply le_log_C2_stima3;
 743              [assumption
 744              |apply lt_sqrt_to_le_times_l;assumption]]]
 745     |rewrite > assoc_plus in ⊢ (? (? % ?) ?);
 746      rewrite > sym_plus in ⊢ (? (? (? ? %) ?) ?);
 747      rewrite > assoc_plus in \vdash (? % ?);
 748      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 749      rewrite > assoc_plus in ⊢ (? (? % ?) ?);
 750      rewrite > assoc_plus in \vdash (? % ?);
 751      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 752      rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 753      rewrite > sym_plus in ⊢ (? (? ? (? (? ? %) ?)) ?);
 754      rewrite < assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 755      rewrite < assoc_plus in \vdash (? % ?);
 756      rewrite < assoc_plus in ⊢ (? (? % ?) ?);
 757      rewrite > assoc_plus in \vdash (? % ?);
 758      rewrite > sym_plus in ⊢ (? (? ? %) ?);
 759      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 760      rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 761      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 762      rewrite > assoc_plus in ⊢ (? (? ? (? ? %)) ?);
 763      simplify in ⊢ (? (? ? (? ? (? ? %))) ?);
 764      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 765      rewrite < assoc_plus in ⊢ (? % ?);apply le_plus_l;
 766      rewrite > assoc_plus in \vdash (? % ?);
 767      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 768      rewrite > sym_plus in ⊢ (? (? ? (? ? %)) ?);
 769      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 770      rewrite < assoc_plus in \vdash (? % ?);apply le_plus_l;
 771      rewrite > assoc_plus in \vdash (? ? %);apply le_n]
 772   |apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1);
 773    apply le_sqrt_n_n]
 774 qed.
 775
 776 lemma eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c).
 777 intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?)
 778  [rewrite > (div_mod (a \mod (b*c)) b)
 779     [rewrite < assoc_plus;
 780      rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?);
 781      rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
 782      rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
 783      rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?);
 784      rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
 785      rewrite > (div_plus_times b)
 786        [rewrite > (div_plus_times c)
 787           [reflexivity
 788           |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %);
 789            apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption]
 790        |apply lt_mod_m_m;assumption]
 791     |assumption]
 792  |unfold lt;rewrite > times_n_SO;apply le_times;assumption]
 793 qed.
 794
 795 lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to
 796                      (prim n) \leq
 797                       2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n)
 798                       +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n)
 799                       + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n)
 800                       +4/(log b n) + 6.
 801 intros;
 802 cut (O < log b n)
 803   [|apply lt_O_log;
 804         [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n))
 805            [apply lt_to_le;assumption
 806            |apply le_sqrt_n_n;]
 807         |apply (trans_le ? (sqrt n))
 808            [apply lt_to_le;assumption
 809            |apply le_sqrt_n_n]]]
 810 apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2)
 811                       +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 812                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
 813                       +4)/(log b n)))
 814   [apply le_times_to_le_div
 815      [assumption
 816      |rewrite > sym_times;apply le_prim_log_stima;assumption]
 817   |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
 818 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 819 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?))
 820      [assumption
 821      |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %);
 822       rewrite > sym_plus in \vdash (? ? (? ? %));
 823       rewrite < assoc_plus in \vdash (? ? %);
 824       apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
 825 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?));
 826          [assumption
 827          |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S;
 828           change in \vdash (? ? (? ? %)) with (1+3);
 829           rewrite < assoc_plus in \vdash (? ? %);
 830           rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
 831           rewrite > assoc_plus in ⊢ (? ? (? % ?));
 832           rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %);
 833           rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus
 834             [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*pred n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*pred (sqrt n)*S (log b 2)) (log b n) ?))
 835                [assumption
 836                |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1);
 837                 rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
 838                 rewrite > assoc_plus in ⊢ (? ? (? % ?));
 839                 rewrite > sym_plus in \vdash (? ? %);
 840                 rewrite < assoc_plus in \vdash (? ? %);
 841                 rewrite > sym_plus in \vdash (? ? (? % ?));
 842                 apply le_plus
 843                   [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
 844                    assumption
 845                   |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
 846                    assumption]]
 847             |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?));
 848                [assumption
 849                |apply le_S_S;apply le_plus
 850                   [rewrite > eq_div_div_div_times;
 851                      [apply le_n
 852                      |*:assumption]
 853                   |rewrite > eq_div_div_div_times
 854                      [apply le_n
 855                      |rewrite > minus_n_O in \vdash (? ? (? %));
 856                       rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus;
 857                       apply (trans_le ? (log b (sqrt n * sqrt n)))
 858                         [elim daemon;
 859                         |apply le_log;
 860                            [assumption
 861                            |elim daemon]]
 862                      |assumption]]]]]]]
 863 qed.
 864
 865 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
 866 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
 867 split
 868   [apply le_O_n
 869   |simplify;reflexivity]
 870 qed.
 871
 872 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
 873 intros.
 874 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
 875 apply le_times_r;unfold sqrt;
 876 apply f_m_to_le_max
 877   [apply le_log_n_n;apply lt_to_le;assumption
 878   |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
 879      [apply (trans_le ? (exp b (log b n)))
 880         [elim (log b n)
 881            [apply le_O_n
 882            |simplify in \vdash (? ? %);
 883            elim (le_to_or_lt_eq ? ? (le_O_n n1))
 884               [elim (le_to_or_lt_eq ? ? H3)
 885                  [apply (trans_le ? (3*(n1*n1)));
 886                     [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
 887                      simplify in \vdash (? % ?);
 888                      simplify;rewrite > sym_plus;
 889                      rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
 890                      rewrite > assoc_plus;apply le_plus_r;
 891                      rewrite < plus_n_Sm;
 892                      rewrite < plus_n_O;
 893                      apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
 894                      apply lt_times_r1;assumption;
 895                     |apply le_times
 896                        [assumption
 897                        |assumption]]
 898                  |rewrite < H4;apply le_times
 899                     [apply lt_to_le;assumption
 900                     |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
 901              |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
 902         |simplify;apply le_exp_log;assumption]
 903      |rewrite < H1;simplify;apply le_n]]
 904 qed.
 905
 906 (* Bertrand weak, lavori in corso
 907
 908 theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n).
 909 intros.
 910 apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?)))
 911   [apply le_n
 912   |unfold sqrt;apply f_m_to_le_max
 913      [do 6 apply lt_to_le;assumption
 914      |apply le_to_leb_true;assumption]
 915   |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n))
 916      [|apply le_S_S_to_le;rewrite < S_pred
 917        [apply le_times_to_le_div2
 918           [apply lt_O_S
 919           |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n);
 920            rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %))));
 921            rewrite > sym_times in \vdash (? ? %);
 922            apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?);
 923            apply lt_times;
 924              [apply lt_O_S
 925              |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]]
 926        |apply le_times_to_le_div;
 927           [apply lt_O_S
 928           |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n)))))
 929              [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n
 930              |change in \vdash (? % ?) with (4 + log 2 n);
 931               rewrite > S_pred in \vdash (? ? (? ? %));
 932                 [change in ⊢ (? ? (? ? %)) with (1 + pred n);
 933                  rewrite > distr_times_plus;apply le_plus_r;elim H
 934                    [simplify;do 3 apply le_S_S;apply le_O_n
 935                    |apply (trans_le ? (log 2 (2*n1)))
 936                       [apply le_log;
 937                          [apply le_S_S;apply le_n
 938                          |rewrite < times_SSO_n;
 939                           change in \vdash (? % ?) with (1 + n1);
 940                           apply le_plus_l;apply (trans_le ? ? ? ? H1);
 941                           apply lt_O_S]
 942                       |apply (trans_le ? (S (4*pred n1)))
 943                          [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?);
 944                           rewrite > log_exp
 945                             [change in \vdash (? ? %) with (1 + (4*pred n1));
 946                              apply le_plus_r;
 947                              assumption
 948                             |apply le_S_S;apply le_n
 949                             |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n]
 950                          |simplify in \vdash (? ? (? ? %));
 951                           rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?);
 952                           rewrite < eq_minus_S_pred;
 953                           rewrite > distr_times_minus;
 954                           change in \vdash (? % ?) with (1 + (4*n1 - 4));
 955                           rewrite > eq_plus_minus_minus_minus
 956                             [simplify;apply le_minus_m;
 957                             |apply lt_O_S
 958                             |rewrite > times_n_SO in \vdash (? % ?);
 959                              apply le_times_r;apply (trans_le ? ? ? ? H1);
 960                              apply lt_O_S]]]]
 961                 |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
 962   apply (trans_le ? ? ? ? Hcut);
 963 *)