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