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 < 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
 210 lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
 211 prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
 212               ((S (S (S (S O))))*n)))/(log b n).
 213 (* la stima del secondo addendo è ottenuta considerando che
 214    logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *)
 215 intros;apply le_times_to_le_div;
 216   [apply lt_O_log;
 217      [apply (trans_le ? b)
 218         [apply lt_to_le;assumption
 219         |assumption]
 220      |assumption]
 221   |apply (trans_le ? (log b (exp n (prim n))))
 222      [rewrite > sym_times;apply log_exp2
 223         [assumption
 224         |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption]
 225      |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O)))))
 226                                *(exp (S (S O)) ((S (S (S (S O))))*n)))))
 227         [apply le_log
 228            [assumption
 229            |apply le_exp_primr;apply (trans_le ? ? ? H H1)]
 230         |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) +
 231                               (log b (exp (S (S O)) ((S (S (S (S O))))*n))))))
 232            [apply log_times;assumption
 233            |apply le_S_S;apply le_plus
 234               [apply log_exp1;assumption
 235               |cases H
 236                  [rewrite > times_n_SO in \vdash (? (? ? %) ?);
 237                   rewrite > log_exp
 238                     [rewrite < plus_n_O;apply le_n
 239                     |apply le_n
 240                     |apply le_n]
 241                  |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O))))))
 242                     [apply log_exp1;apply le_S;assumption
 243                     |rewrite > times_n_SO in \vdash (? ? %);
 244                      apply le_times_r;apply le_S_S;
 245                      rewrite > lt_to_log_O
 246                        [apply le_n
 247                        |apply lt_O_S
 248                        |apply le_S_S;assumption]]]]]]]]
 249 qed.
 250
 251 theorem le_log_C2_stima : \forall n,b. S O < b \to b*b < n \to
 252 log b (C2 n) \leq
 253 (*(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +*)
 254 ((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 255               ((S (S (S (S O))))*n)))/(log b n)) +
 256 (((S (((S (S (S (S O))))*(S (log b (pred n)))) +
 257               ((S (S (S (S O))))*n)))/(log b n)) +
 258  (((sigma_p n (\lambda x.leb (S n) (x*x))
 259               (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
 260               ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
 261   *(S (log b (S (S (S O))))))/n!)).intros.
 262 apply (trans_le ? ? ? (le_log_C2_sigma_p ? ? ?))
 263   [assumption
 264   |apply le_plus
 265      [apply (trans_le ? ? ? ? (le_prim_n_stima ? ? ? ?));
 266       [unfold prim;apply le_sigma_p1;intros;
 267        do 2 rewrite < times_n_SO;elim (primeb i)
 268         [elim (leb (S n) (i*i));simplify [apply le_n|apply le_O_n]
 269         |simplify;apply le_n]
 270       |assumption
 271       |apply (trans_le ? ? ? ? H1);apply le_S;apply le_times_n;
 272        apply lt_to_le;assumption]
 273    |apply le_plus
 274      [apply le_prim_n_stima;
 275        [assumption
 276        |apply (trans_le ? (b*b))
 277           [apply le_times_n;apply lt_to_le;assumption
 278           |apply lt_to_le;assumption]]
 279      |apply monotonic_div
 280         [apply lt_O_fact
 281         |apply le_times_l;apply le_sigma_p;intros;apply le_times_l;
 282          apply le_prim_n_stima
 283            [assumption
 284            |apply (le_exp_to_le1 ? ? (S (S O)));
 285               [apply le_S;apply le_n
 286               |do 2 rewrite > exp_SSO;apply (trans_le ? n)
 287                  [apply lt_to_le;assumption
 288                  |apply lt_to_le;apply leb_true_to_le;assumption]]]]]]]
 289 qed.
 290
 291 lemma log_interval : \forall b,k,n. S O < b \to exp b k \leq n \to n < exp b (S k) \to
 292                        log b n = k.
 293 intros 2.elim k
 294   [simplify in H2;rewrite < times_n_SO in H2;apply lt_to_log_O;assumption
 295   |cut (log b n1 < S (S n))
 296      [cut (n < log b n1)
 297         [apply antisymmetric_le
 298            [apply le_S_S_to_le;assumption
 299            |assumption]
 300         |apply (trans_le ? (log b (exp b (S n))))
 301            [rewrite > eq_log_exp
 302               [apply le_n
 303               |assumption]
 304            |apply le_log;assumption]]
 305      |apply le_S_S;apply (trans_le ? (log b (pred (exp b (S (S n))))))
 306         [apply le_log
 307            [assumption
 308            |apply le_S_S_to_le;apply (trans_le ? ? ? H3);
 309             rewrite > minus_n_O in \vdash (? ? (? (? %)));
 310             rewrite < (eq_minus_S_pred (exp b (S (S n))) O);
 311             rewrite > minus_n_O in \vdash (? % ?);
 312             apply minus_le_S_minus_S]
 313         |unfold log;apply f_false_to_le_max;
 314            [apply (ex_intro ? ? (S n));split
 315               [apply (trans_le ? (exp b (S n)));
 316                  [apply lt_to_le;apply lt_m_exp_nm;assumption
 317                  |rewrite > minus_n_O in ⊢ (? ? (? %));
 318                   rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
 319                   rewrite > sym_plus;
 320                   change in \vdash (? % ?) with (S (O + exp b (S n)));
 321                   apply lt_minus_to_plus;
 322                   change in ⊢ (? ? (? % ?)) with (b * (exp b (S n)));
 323                   rewrite > times_n_SO in \vdash (? ? (? ? %));
 324                   rewrite > sym_times in \vdash (? ? (? % ?));
 325                   rewrite < distributive_times_minus;unfold lt;
 326                   rewrite > times_n_SO in \vdash (? % ?);apply le_times
 327                     [apply lt_O_exp;apply (trans_le ? ? ? ? H1);
 328                      apply le_S;apply le_n
 329                     |apply le_plus_to_minus_r;simplify;assumption]]
 330               |apply le_to_leb_true;
 331                rewrite > minus_n_O in \vdash (? ? (? %));
 332                rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
 333                rewrite > sym_plus;change in \vdash (? % ?) with (S (exp b (S n)));
 334                apply lt_exp;
 335                  [assumption
 336                  |apply le_n]]
 337            |intros;apply lt_to_leb_false;unfold lt;
 338             rewrite > minus_n_O in \vdash (? (? (? %)) ?);
 339             rewrite < eq_minus_S_pred;rewrite < minus_Sn_m
 340               [rewrite > minus_S_S;rewrite < minus_n_O;apply le_exp;
 341                  [apply (trans_le ? ? ? ? H1);apply le_S;apply le_n
 342                  |assumption]
 343               |apply lt_O_exp;apply (trans_le ? ? ? ? H1);apply le_S;apply le_n]]]]]
 344 qed.
 345
 346 lemma log_strano : \forall b,i.S O < b \to S O < i \to
 347                   ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
 348                   (S (S (S O)))*i.
 349 alias num (instance 0) = "natural number".
 350 cut (\forall b,i,k.S O < b \to S O < i \to
 351             (exp b k) \leq i-1 \to i-1 < (exp b (S k)) \to
 352                   ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
 353                   (S (S (S O)))*i)
 354   [intros;apply (Hcut ? ? (log b (i-1)) H H1);
 355      [apply le_exp_log;rewrite > (minus_n_n 1) in \vdash (? % ?);
 356       apply lt_plus_to_lt_minus;
 357         [apply le_n
 358         |rewrite < eq_minus_plus_plus_minus
 359            [rewrite > sym_plus;rewrite > eq_minus_plus_plus_minus;
 360               [rewrite < minus_n_n;rewrite < plus_n_O;assumption
 361               |apply le_n]
 362            |apply lt_to_le;assumption]]
 363      |apply lt_exp_log;assumption]
 364   |intros;rewrite > minus_n_O in ⊢ (? (? (? ? (? ? (? %))) ?) ?);
 365    rewrite < eq_minus_S_pred;rewrite > (log_interval ? k)
 366      [apply (trans_le ? (3*(exp b k) + 3))
 367         [change in \vdash (? (? ? %) ?) with (2+3);
 368          rewrite < assoc_plus;apply le_plus_l;
 369          elim k
 370            [simplify;apply le_S;apply le_n
 371            |elim (decidable_eq_nat O n)
 372               [rewrite < H5;apply (trans_le ? (3*(exp 2 1)));
 373                  [simplify;apply le_n
 374                  |apply le_times_r;apply monotonic_exp1;assumption]
 375               |rewrite < times_n_Sm;apply (trans_le ? (3*(exp b n) + 4))
 376                  [rewrite > assoc_plus;rewrite > sym_plus;apply le_plus_l;
 377                   assumption
 378                  |rewrite < sym_plus;change in \vdash (? % ?) with (S (3 + (3*(exp b n))));
 379                   apply lt_minus_to_plus;
 380                   change in ⊢ (? ? (? (? ? %) ?)) with (b*(exp b n));
 381                   rewrite > sym_times in \vdash (? ? (? (? ? %) ?));
 382                   rewrite < assoc_times;
 383                   rewrite > times_n_SO in ⊢ (? ? (? ? (? ? %)));
 384                   rewrite < assoc_times;rewrite < distr_times_minus;
 385                   apply (trans_le ? (3*2*1))
 386                     [simplify;apply le_S;apply le_S;apply le_n
 387                     |apply le_times
 388                        [apply le_times_r;apply (trans_le ? (exp 2 n))
 389                           [rewrite > exp_n_SO in \vdash (? % ?);apply le_exp
 390                              [apply le_S;apply le_n
 391                              |generalize in match H5;cases n
 392                                 [intro;elim H6;reflexivity
 393                                 |intro;apply le_S_S;apply le_O_n]]
 394                           |apply monotonic_exp1;assumption]
 395                        |apply le_S_S_to_le;rewrite < minus_Sn_m;
 396                           [simplify;rewrite < minus_n_O;assumption
 397                           |apply lt_to_le;assumption]]]]]]
 398         |rewrite > times_n_SO in \vdash (? (? ? %) ?);
 399          rewrite < distr_times_plus;apply le_times_r;
 400          rewrite < plus_n_SO;apply (trans_le ? (S (i-1)))
 401            [apply le_S_S;assumption
 402            |rewrite < minus_Sn_m
 403               [simplify;rewrite < minus_n_O;apply le_n
 404               |apply lt_to_le;assumption]]]
 405      |assumption
 406      |assumption
 407      |assumption]]
 408 qed.
 409
 410 alias num (instance 0) = "natural number".
 411 lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
 412             (sigma_p n (\lambda x.leb (S n) (x*x))
 413               (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
 414               ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
 415             \leq ((28 * n * n!)/(pred (log b n))).
 416 intros.apply (trans_le ? (sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i. ((7*i)/(log b i))*(S (n!/i)))))
 417   [apply le_sigma_p;intros;cut (b \leq i)
 418      [cut (1 < i) [|apply (trans_le ? ? ? H Hcut)]
 419       apply le_times_l;apply monotonic_div
 420         [apply lt_O_log
 421            [generalize in match H3;cases i
 422               [simplify;intros;destruct H4
 423               |intro;apply le_S_S;apply le_O_n]
 424            |assumption]
 425         |rewrite > sym_times;simplify in ⊢ (? (? (? % ?)) ?);
 426          change in ⊢ (? % ?) with (1 + ((4 + (log b (pred i) * 4)) + 4*i));
 427          rewrite > assoc_plus;rewrite < assoc_plus;
 428          simplify in \vdash (? (? % ?) ?);rewrite < assoc_plus;
 429          apply (trans_le ? (3*i + 4*i))
 430            [apply le_minus_to_plus;rewrite > eq_minus_plus_plus_minus
 431               [rewrite < minus_n_n;rewrite < plus_n_O;
 432                rewrite > sym_plus;rewrite > sym_times;apply log_strano
 433                  [assumption
 434                  |lapply (leb_true_to_le ? ? H3);apply (trans_le ? ? ? H);
 435                   apply (le_exp_to_le1 ? ? 2);
 436                     [apply le_S_S;apply le_O_n
 437                     |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 438                      apply lt_to_le;assumption]]
 439               |apply le_n]
 440            |rewrite > sym_times in \vdash (? (? % ?) ?);
 441             rewrite > sym_times in \vdash (? (? ? %) ?);
 442             rewrite < distr_times_plus;rewrite > sym_times;apply le_n]]
 443      |apply (le_exp_to_le1 ? ? 2);
 444         [apply le_S_S;apply le_O_n
 445         |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 446          apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
 447          apply le_n]]
 448   |apply (trans_le ? (sigma_p n (λx:nat.leb (S n) (x*x)) (λi:nat.7*i/log b i*((2*(n!))/i))))
 449      [apply le_sigma_p;intros;apply le_times_r;apply (trans_le ? (n!/i + n!/i))
 450         [change in \vdash (? % ?) with (1 + n!/i);apply le_plus_l;
 451          apply le_times_to_le_div
 452            [generalize in match H3;cases i;simplify;intro
 453               [destruct H4
 454               |apply le_S_S;apply le_O_n]
 455            |generalize in match H2;cases n;intro
 456               [elim (not_le_Sn_O ? H4)
 457               |change in \vdash (? ? %) with ((S n1)*(n1!));apply le_times
 458                  [apply lt_to_le;assumption
 459                  |apply lt_O_fact]]]
 460         |rewrite > plus_n_O in \vdash (? (? ? %) ?);
 461          change in \vdash (? % ?) with (2 * (n!/i));
 462          apply le_times_div_div_times;
 463          generalize in match H3;cases i;simplify;intro
 464            [destruct H4
 465            |apply le_S_S;apply le_O_n]]
 466      |apply (trans_le ? (sigma_p n (\lambda x:nat.leb (S n) (x*x)) (\lambda i.((14*(n!))/log b i))))
 467         [apply le_sigma_p;intros;
 468          cut (b \leq i)
 469            [|apply (le_exp_to_le1 ? ? 2);
 470               [apply le_S_S;apply le_O_n
 471               |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
 472                apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
 473                apply le_n]]
 474          cut (1 < i)
 475            [|apply (trans_le ? ? ? H Hcut)]
 476          change in ⊢ (? ? (? % ?)) with ((7*2)*(n!));
 477          rewrite > assoc_times in \vdash (? ? (? % ?));
 478          apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?));
 479            [apply lt_to_le;assumption
 480            |rewrite > (eq_div_div_times ? ? 7)
 481               [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
 482                rewrite < assoc_times in \vdash (? (? % ?) ?);
 483                apply (trans_le ? ? ? (le_div_times_m ? ? ? ? ?))
 484                  [apply lt_O_log
 485                     [apply lt_to_le;assumption
 486                     |assumption]
 487                  |unfold lt;rewrite > times_n_SO in \vdash (? % ?);
 488                   apply le_times;
 489                     [apply le_S_S;apply le_O_n
 490                     |apply lt_to_le;assumption]
 491                  |apply le_n]
 492               |apply le_S_S;apply le_O_n
 493               |apply lt_to_le;assumption]]
 494         |apply (trans_le ? (sigma_p (S n) (\lambda x.leb (S n) (x*x))
 495                       (\lambda i.14*n!/log b i)))
 496            [apply (bool_elim ? (leb (S n) (n*n)));intro
 497               [rewrite > true_to_sigma_p_Sn
 498                  [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
 499                   apply le_plus_r;apply le_O_n
 500                  |assumption]
 501               |rewrite > false_to_sigma_p_Sn
 502                  [apply le_n
 503                  |assumption]]
 504            |apply (trans_le ? ? ? (le_sigma_p_div_log_div_pred_log ? ? ? ? ?));
 505               [assumption
 506               |apply lt_to_le;assumption
 507               |rewrite < assoc_times;
 508                rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?);
 509                rewrite < assoc_times;apply le_n]]]]]
 510 qed.
 511
 512 theorem le_log_C2_stima2 : \forall n,b. S O < b \to b*b < n \to
 513 log b (C2 n) \leq
 514 (14*n/(log b n)) +
 515  ((((28*n*n!)/pred (log b n))
 516   *(S (log b (S (S (S O))))))/n!).intros.
 517 apply (trans_le ? ? ? (le_log_C2_stima ? ? H H1));
 518 rewrite < assoc_plus in \vdash (? % ?);apply le_plus
 519   [rewrite > times_SSO_n in \vdash (? % ?);
 520    apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?))
 521      [apply lt_O_log
 522        [apply (trans_le ? (b*b))
 523           [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
 524           |apply lt_to_le;assumption]
 525        |apply (trans_le ? (b*b))
 526           [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 527              [apply le_n|apply lt_to_le;assumption]
 528           |apply lt_to_le;assumption]]
 529      |change in \vdash (? ? (? (? % ?) ?)) with (2*7);
 530       apply monotonic_div;
 531         [apply lt_O_log
 532           [apply (trans_le ? (b*b))
 533              [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
 534              |apply lt_to_le;assumption]
 535           |apply (trans_le ? (b*b))
 536              [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 537                 [apply le_n|apply lt_to_le;assumption]
 538              |apply lt_to_le;assumption]]
 539         |rewrite > assoc_times;apply le_times_r;
 540          change in \vdash (? (? (? (? ? %) ?)) ?) with (1 + (log b (pred n)));
 541          rewrite > distr_times_plus;
 542          change in \vdash (? % ?) with (1 + (4*1+4*log b (pred n)+4*n));
 543          do 2 rewrite < assoc_plus;simplify in ⊢ (? (? (? % ?) ?) ?);
 544          change in ⊢ (? ? %) with ((3+4)*n);rewrite > sym_times in \vdash (? ? %);
 545          rewrite > distr_times_plus;
 546          rewrite > sym_times in \vdash (? ? (? % ?));
 547          rewrite > sym_times in \vdash (? ? (? ? %));
 548          apply le_plus_l;rewrite > sym_plus;apply log_strano
 549            [assumption
 550            |apply (trans_le ? ? ? H);apply (trans_le ? (b*b))
 551               [rewrite > times_n_SO in \vdash (? % ?);
 552                apply le_times_r;apply lt_to_le;assumption
 553               |apply lt_to_le;assumption]]]]
 554   |apply monotonic_div
 555      [apply lt_O_fact
 556      |apply le_times_l;apply (le_sigma_p_lemma1 ? ? H H1)]]
 557 qed.
 558
 559 theorem le_log_C2_stima3 : \forall n,b. S O < b \to b*b < n \to
 560 log b (C2 n) \leq
 561 (14*n/(log b n)) +
 562  ((28*n)*(S (log b (S (S (S O)))))/pred (log b n)).intros.
 563 apply (trans_le ? ? ? (le_log_C2_stima2 ? ? H H1));apply le_plus_r;
 564 (*apply (trans_le ? ((28*n)*(28*n*n!/pred (log b n)*S (log b 3)/(28*n*n!))))
 565   [*)
 566 rewrite > (eq_div_div_times ? ? (28*n)) in \vdash (? % ?)
 567   [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
 568    rewrite < assoc_times;
 569    apply le_div_times_m;
 570      [apply (trans_le ? (pred (log b (b*b))))
 571         [rewrite < exp_SSO;rewrite > eq_log_exp;
 572            [apply le_n
 573            |assumption]
 574         |rewrite < exp_SSO;rewrite > eq_log_exp;
 575            [simplify;rewrite > minus_n_O in \vdash (? ? (? %));
 576             rewrite < eq_minus_S_pred;
 577             apply le_plus_to_minus_r;simplify;
 578             rewrite < (eq_log_exp b 2);
 579               [apply le_log
 580                  [assumption
 581                  |rewrite > exp_SSO;apply lt_to_le;assumption]
 582               |assumption]
 583            |assumption]]
 584      |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
 585         [rewrite > times_n_SO in \vdash (? % ?);apply le_times
 586            [apply le_S_S;apply le_O_n
 587            |apply (trans_le ? ? ? ? H1);apply le_S_S;
 588             rewrite > times_n_SO;apply le_times
 589               [apply le_O_n
 590               |apply lt_to_le;assumption]]
 591         |apply lt_O_fact]]
 592   |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
 593      [apply le_S_S;apply le_O_n
 594      |apply (trans_le ? ? ? ? H1);apply le_S_S;
 595       rewrite > times_n_SO;apply le_times
 596         [apply le_O_n
 597         |apply lt_to_le;assumption]]
 598   |apply lt_O_fact]
 599 qed.
 600
 601 lemma le_prim_log1: \forall n,b. S O < b \to O < n \to
 602                      (prim n)*(log b n) \leq
 603                      log b (A n) + log b (C1 n) + log b (C2 n) + 2.
 604 intros.change in \vdash (? ? (? ? %)) with (1+1).
 605 rewrite < assoc_plus;rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)).
 606 rewrite > assoc_plus in ⊢ (? ? (? % ?));
 607 apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1));
 608   [apply (trans_le ? (log b (A n * (C1 n * C2 n))))
 609      [apply (trans_le ? (log b (exp n (prim n))))
 610         [apply log_exp2;assumption
 611         |apply le_log
 612            [assumption
 613            |rewrite < jj;apply asdasd]]
 614      |rewrite > sym_plus;simplify;apply log_times;assumption]
 615   |apply le_plus_l;apply le_plus_r;rewrite > sym_plus;simplify;apply log_times;
 616    assumption]
 617 qed.
 618
 619 lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to
 620                   log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1.
 621 intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n))))))
 622   [apply le_log
 623      [assumption
 624      |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption]
 625   |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n)))))));
 626      [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n)))));
 627       apply log_times;assumption
 628      |apply le_plus_r;apply le_plus;apply log_exp1;assumption]]
 629 qed.
 630
 631 lemma le_theta_pi_A : \forall n.theta_pi n \leq A n.
 632 intro.unfold theta_pi.unfold A.apply le_pi_p.intros.
 633 rewrite > exp_n_SO in \vdash (? % ?).
 634 cut (O < i)
 635   [apply le_exp
 636      [assumption
 637      |apply lt_O_log
 638         [apply (trans_le ? ? ? Hcut);apply le_S_S_to_le;assumption
 639         |apply le_S_S_to_le;assumption]]
 640   |apply prime_to_lt_O;apply primeb_true_to_prime;assumption]
 641 qed.
 642
 643 definition sqrt \def
 644   \lambda n.max n (\lambda x.leb (x*x) n).
 645
 646 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
 647 intros;apply (trans_le ? (sqrt m * sqrt m))
 648   [apply le_times;assumption
 649   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
 650    apply (ex_intro ? ? O);split
 651      [apply le_O_n
 652      |simplify;reflexivity]]
 653 qed.
 654
 655 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
 656 intros;apply (trans_le ? (sqrt m * sqrt m))
 657   [apply (trans_le ? (S n * S n))
 658      [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
 659         [apply le_times_r;apply le_S;apply le_n
 660         |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
 661          apply le_plus_r;apply le_O_n]
 662      |apply le_times;assumption]
 663   |apply le_sqrt_to_le_times_l;apply le_n]
 664 qed.
 665
 666 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
 667 intros;apply not_le_to_lt;intro;
 668 apply ((leb_false_to_not_le ? ?
 669            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
 670          H1);
 671 apply (trans_le ? ? ? ? H1);cases n
 672   [apply le_n
 673   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
 674      [apply le_S_S;apply le_O_n
 675      |apply le_n]]
 676 qed.
 677
 678 theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n.
 679 intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n))
 680   [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n)
 681      [simplify;reflexivity
 682      |apply (bool_elim ? (primeb (S n1)))
 683         [intro;rewrite > true_to_pi_p_Sn
 684            [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %)
 685               [apply eq_f2
 686                  [reflexivity
 687                  |apply H;intros;apply H1;apply le_S;assumption]
 688               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 689                rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n]
 690            |assumption]
 691         |intro;rewrite > false_to_pi_p_Sn
 692            [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %)
 693               [apply H;intros;apply H1;apply le_S;assumption
 694               |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
 695                rewrite > H2;whd;reflexivity]
 696            |assumption]]]
 697   |apply le_S_S;unfold sqrt;apply le_max_n
 698   |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify
 699      [rewrite > lt_to_leb_false
 700         [reflexivity
 701         |apply le_sqrt_to_le_times_r;assumption]
 702      |reflexivity]]
 703 qed.
 704
 705 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
 706 intro.unfold sqrt.apply le_max_n.
 707 qed.
 708
 709 lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to
 710                      (prim n)*(log b n) \leq
 711                       2*S (log b (pred n))+2*(pred n)*S (log b 2)
 712                       +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 713                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
 714                       +4.
 715 intros.cut (1 < n)
 716   [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) +
 717                      (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) +
 718                      ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2))
 719     [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?))
 720        [apply lt_to_le;assumption
 721        |apply le_plus_l;apply le_plus
 722           [apply le_plus
 723              [apply le_log_A1;assumption
 724              |rewrite < eq_theta_pi_sqrt_C1;apply (trans_le ? (log b (A (sqrt n))))
 725                 [apply le_log
 726                    [assumption
 727                    |apply le_theta_pi_A]
 728                 |apply le_log_A1
 729                    [assumption
 730                    |apply (trans_le ? ? ? H);apply lt_to_le;assumption]]]
 731           |apply le_log_C2_stima3;
 732              [assumption
 733              |apply lt_sqrt_to_le_times_l;assumption]]]
 734     |rewrite > assoc_plus in ⊢ (? (? % ?) ?);
 735      rewrite > sym_plus in ⊢ (? (? (? ? %) ?) ?);
 736      rewrite > assoc_plus in \vdash (? % ?);
 737      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 738      rewrite > assoc_plus in ⊢ (? (? % ?) ?);
 739      rewrite > assoc_plus in \vdash (? % ?);
 740      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 741      rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 742      rewrite > sym_plus in ⊢ (? (? ? (? (? ? %) ?)) ?);
 743      rewrite < assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 744      rewrite < assoc_plus in \vdash (? % ?);
 745      rewrite < assoc_plus in ⊢ (? (? % ?) ?);
 746      rewrite > assoc_plus in \vdash (? % ?);
 747      rewrite > sym_plus in ⊢ (? (? ? %) ?);
 748      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 749      rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
 750      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 751      rewrite > assoc_plus in ⊢ (? (? ? (? ? %)) ?);
 752      simplify in ⊢ (? (? ? (? ? (? ? %))) ?);
 753      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 754      rewrite < assoc_plus in ⊢ (? % ?);apply le_plus_l;
 755      rewrite > assoc_plus in \vdash (? % ?);
 756      rewrite > assoc_plus in ⊢ (? (? ? %) ?);
 757      rewrite > sym_plus in ⊢ (? (? ? (? ? %)) ?);
 758      rewrite < assoc_plus in ⊢ (? (? ? %) ?);
 759      rewrite < assoc_plus in \vdash (? % ?);apply le_plus_l;
 760      rewrite > assoc_plus in \vdash (? ? %);apply le_n]
 761   |apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1);
 762    apply le_sqrt_n_n]
 763 qed.
 764
 765 lemma eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c).
 766 intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?)
 767  [rewrite > (div_mod (a \mod (b*c)) b)
 768     [rewrite < assoc_plus;
 769      rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?);
 770      rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
 771      rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
 772      rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?);
 773      rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
 774      rewrite > (div_plus_times b)
 775        [rewrite > (div_plus_times c)
 776           [reflexivity
 777           |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %);
 778            apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption]
 779        |apply lt_mod_m_m;assumption]
 780     |assumption]
 781  |unfold lt;rewrite > times_n_SO;apply le_times;assumption]
 782 qed.
 783
 784 lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to
 785                      (prim n) \leq
 786                       2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n)
 787                       +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n)
 788                       + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n)
 789                       +4/(log b n) + 6.
 790 intros;
 791 cut (O < log b n)
 792   [|apply lt_O_log;
 793         [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n))
 794            [apply lt_to_le;assumption
 795            |apply le_sqrt_n_n;]
 796         |apply (trans_le ? (sqrt n))
 797            [apply lt_to_le;assumption
 798            |apply le_sqrt_n_n]]]
 799 apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2)
 800                       +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 801                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
 802                       +4)/(log b n)))
 803   [apply le_times_to_le_div
 804      [assumption
 805      |rewrite > sym_times;apply le_prim_log_stima;assumption]
 806   |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
 807 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 808 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?))
 809      [assumption
 810      |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %);
 811       rewrite > sym_plus in \vdash (? ? (? ? %));
 812       rewrite < assoc_plus in \vdash (? ? %);
 813       apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
 814 +(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) ?));
 815          [assumption
 816          |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S;
 817           change in \vdash (? ? (? ? %)) with (1+3);
 818           rewrite < assoc_plus in \vdash (? ? %);
 819           rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
 820           rewrite > assoc_plus in ⊢ (? ? (? % ?));
 821           rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %);
 822           rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus
 823             [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) ?))
 824                [assumption
 825                |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1);
 826                 rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
 827                 rewrite > assoc_plus in ⊢ (? ? (? % ?));
 828                 rewrite > sym_plus in \vdash (? ? %);
 829                 rewrite < assoc_plus in \vdash (? ? %);
 830                 rewrite > sym_plus in \vdash (? ? (? % ?));
 831                 apply le_plus
 832                   [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
 833                    assumption
 834                   |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
 835                    assumption]]
 836             |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?));
 837                [assumption
 838                |apply le_S_S;apply le_plus
 839                   [rewrite > eq_div_div_div_times;
 840                      [apply le_n
 841                      |*:assumption]
 842                   |rewrite > eq_div_div_div_times
 843                      [apply le_n
 844                      |rewrite > minus_n_O in \vdash (? ? (? %));
 845                       rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus;
 846                       apply (trans_le ? (log b (sqrt n * sqrt n)))
 847                         [elim daemon;
 848                         |apply le_log;
 849                            [assumption
 850                            |elim daemon]]
 851                      |assumption]]]]]]]
 852 qed.
 853
 854 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
 855 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
 856 split
 857   [apply le_O_n
 858   |simplify;reflexivity]
 859 qed.
 860
 861 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
 862 intros.
 863 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
 864 apply le_times_r;unfold sqrt;
 865 apply f_m_to_le_max
 866   [apply le_log_n_n;apply lt_to_le;assumption
 867   |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
 868      [apply (trans_le ? (exp b (log b n)))
 869         [elim (log b n)
 870            [apply le_O_n
 871            |simplify in \vdash (? ? %);
 872            elim (le_to_or_lt_eq ? ? (le_O_n n1))
 873               [elim (le_to_or_lt_eq ? ? H3)
 874                  [apply (trans_le ? (3*(n1*n1)));
 875                     [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
 876                      simplify in \vdash (? % ?);
 877                      simplify;rewrite > sym_plus;
 878                      rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
 879                      rewrite > assoc_plus;apply le_plus_r;
 880                      rewrite < plus_n_Sm;
 881                      rewrite < plus_n_O;
 882                      apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
 883                      apply lt_times_r1;assumption;
 884                     |apply le_times
 885                        [assumption
 886                        |assumption]]
 887                  |rewrite < H4;apply le_times
 888                     [apply lt_to_le;assumption
 889                     |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
 890              |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
 891         |simplify;apply le_exp_log;assumption]
 892      |rewrite < H1;simplify;apply le_n]]
 893 qed.
 894
 895 (* Bertrand weak, lavori in corso
 896
 897 theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n).
 898 intros.
 899 apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?)))
 900   [apply le_n
 901   |unfold sqrt;apply f_m_to_le_max
 902      [do 6 apply lt_to_le;assumption
 903      |apply le_to_leb_true;assumption]
 904   |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n))
 905      [|apply le_S_S_to_le;rewrite < S_pred
 906        [apply le_times_to_le_div2
 907           [apply lt_O_S
 908           |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n);
 909            rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %))));
 910            rewrite > sym_times in \vdash (? ? %);
 911            apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?);
 912            apply lt_times;
 913              [apply lt_O_S
 914              |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]]
 915        |apply le_times_to_le_div;
 916           [apply lt_O_S
 917           |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n)))))
 918              [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n
 919              |change in \vdash (? % ?) with (4 + log 2 n);
 920               rewrite > S_pred in \vdash (? ? (? ? %));
 921                 [change in ⊢ (? ? (? ? %)) with (1 + pred n);
 922                  rewrite > distr_times_plus;apply le_plus_r;elim H
 923                    [simplify;do 3 apply le_S_S;apply le_O_n
 924                    |apply (trans_le ? (log 2 (2*n1)))
 925                       [apply le_log;
 926                          [apply le_S_S;apply le_n
 927                          |rewrite < times_SSO_n;
 928                           change in \vdash (? % ?) with (1 + n1);
 929                           apply le_plus_l;apply (trans_le ? ? ? ? H1);
 930                           apply lt_O_S]
 931                       |apply (trans_le ? (S (4*pred n1)))
 932                          [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?);
 933                           rewrite > log_exp
 934                             [change in \vdash (? ? %) with (1 + (4*pred n1));
 935                              apply le_plus_r;
 936                              assumption
 937                             |apply le_S_S;apply le_n
 938                             |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n]
 939                          |simplify in \vdash (? ? (? ? %));
 940                           rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?);
 941                           rewrite < eq_minus_S_pred;
 942                           rewrite > distr_times_minus;
 943                           change in \vdash (? % ?) with (1 + (4*n1 - 4));
 944                           rewrite > eq_plus_minus_minus_minus
 945                             [simplify;apply le_minus_m;
 946                             |apply lt_O_S
 947                             |rewrite > times_n_SO in \vdash (? % ?);
 948                              apply le_times_r;apply (trans_le ? ? ? ? H1);
 949                              apply lt_O_S]]]]
 950                 |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
 951   apply (trans_le ? ? ? ? Hcut);
 952 *)
 953 *)