]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/chebyshev.ma
exercises ready
[helm.git] / helm / software / matita / library / nat / chebyshev.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/log.ma".
16 include "nat/pi_p.ma".
17 include "nat/factorization.ma".
18 include "nat/factorial2.ma".
19
20 definition prim: nat \to nat \def
21 \lambda n. sigma_p (S n) primeb (\lambda p.1).
22
23 theorem le_prim_n: \forall n. prim n \le n.
24 intros.unfold prim. elim n
25   [apply le_n
26   |apply (bool_elim ? (primeb (S n1)));intro
27     [rewrite > true_to_sigma_p_Sn
28       [rewrite > sym_plus.
29        rewrite < plus_n_Sm.
30        rewrite < plus_n_O.
31        apply le_S_S.assumption
32       |assumption
33       ]
34     |rewrite > false_to_sigma_p_Sn
35       [apply le_S.assumption
36       |assumption
37       ]
38     ]
39   ]
40 qed.
41
42 theorem not_prime_times_SSO: \forall n. 1 < n \to \lnot prime (2*n).
43 intros.intro.elim H1.
44 absurd (2 = 2*n)
45   [apply H3
46     [apply (witness ? ? n).reflexivity
47     |apply le_n
48     ]
49   |apply lt_to_not_eq.
50    rewrite > times_n_SO in ⊢ (? % ?).
51    apply lt_times_r.
52    assumption
53   ]
54 qed.
55
56 theorem eq_prim_prim_pred: \forall n. 1 < n \to 
57 (prim (2*n)) = (prim (pred (2*n))).
58 intros.unfold prim.
59 rewrite < S_pred
60   [rewrite > false_to_sigma_p_Sn
61     [reflexivity
62     |apply not_prime_to_primeb_false.
63      apply not_prime_times_SSO.
64      assumption
65     ]
66   |apply (trans_lt ? (2*1))
67     [simplify.apply lt_O_S
68     |apply lt_times_r.
69      assumption
70     ]
71   ]
72 qed.
73
74 theorem le_prim_n1: \forall n. 4 \le n \to prim (S(2*n)) \le n.
75 intros.unfold prim. elim H
76   [simplify.apply le_n
77   |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1))
78     [apply (bool_elim ? (primeb (S(2*(S n1)))));intro
79       [rewrite > true_to_sigma_p_Sn
80         [rewrite > sym_plus.
81          rewrite < plus_n_Sm.
82          rewrite < plus_n_O.
83          apply le_S_S.
84          rewrite < Hcut.
85          rewrite > times_SSO.
86          assumption
87         |assumption
88         ]
89       |rewrite > false_to_sigma_p_Sn
90         [apply le_S.
91          rewrite < Hcut.
92          rewrite > times_SSO.
93          assumption
94         |assumption
95         ]
96       ]
97     |apply sym_eq.apply (eq_prim_prim_pred (S n1)).
98      apply le_S_S.apply (trans_le ? 4)
99       [apply leb_true_to_le.reflexivity
100       |assumption
101       ]
102     ]
103   ]
104 qed.
105
106 (* usefull to kill a successor in bertrand *) 
107 theorem le_prim_n2: \forall n. 7 \le n \to prim (S(2*n)) \le pred n.
108 intros.unfold prim. elim H
109   [apply leb_true_to_le.reflexivity.
110   |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1))
111     [apply (bool_elim ? (primeb (S(2*(S n1)))));intro
112       [rewrite > true_to_sigma_p_Sn
113         [rewrite > sym_plus.
114          rewrite < plus_n_Sm.
115          rewrite < plus_n_O.
116          simplify in  ⊢ (? ? %).
117          rewrite > S_pred in ⊢ (? ? %)
118           [apply le_S_S.
119            rewrite < Hcut.
120            rewrite > times_SSO.
121            assumption
122           |apply (ltn_to_ltO ? ? H1)
123           ]
124         |assumption
125         ]
126       |rewrite > false_to_sigma_p_Sn
127         [simplify in  ⊢ (? ? %).
128          apply (trans_le ? ? ? ? (le_pred_n n1)).
129          rewrite < Hcut.
130          rewrite > times_SSO.
131          assumption
132         |assumption
133         ]
134       ]
135     |apply sym_eq.apply (eq_prim_prim_pred (S n1)).
136      apply le_S_S.apply (trans_le ? 4)
137       [apply leb_true_to_le.reflexivity
138       |apply (trans_le ? ? ? ? H1).
139        apply leb_true_to_le.reflexivity
140       ]
141     ]
142   ]
143 qed.
144
145 (* da spostare *)
146 theorem le_pred: \forall n,m. n \le m \to pred n \le pred m.
147 apply nat_elim2;intros
148   [apply le_O_n
149   |apply False_ind.apply (le_to_not_lt ? ? H).
150    apply lt_O_S
151   |simplify.apply le_S_S_to_le.assumption
152   ]
153 qed.
154
155 (* la prova potrebbe essere migliorata *)
156 theorem le_prim_n3: \forall n. 15 \le n \to
157 prim n \le pred (n/2).
158 intros.
159 elim (or_eq_eq_S (pred n)).
160 elim H1
161   [cut (n = S (2*a))
162     [rewrite > Hcut.
163      apply (trans_le ? (pred a))
164       [apply le_prim_n2.
165        apply (le_times_to_le 2)
166         [apply le_n_Sn
167         |apply le_S_S_to_le.
168          rewrite < Hcut.
169          assumption
170         ]
171       |apply le_pred.
172        apply le_times_to_le_div
173         [apply lt_O_S
174         |apply le_n_Sn
175         ]
176       ]
177     |rewrite < H2.
178      apply S_pred.
179      apply (ltn_to_ltO ? ? H)
180     ]
181   |cut (n=2*(S a))
182     [rewrite > Hcut.
183      rewrite > eq_prim_prim_pred
184       [rewrite > times_SSO in ⊢ (? % ?).
185        change in ⊢ (? (? %) ?) with (S (2*a)).
186        rewrite > sym_times in ⊢ (? ? (? (? % ?))).
187        rewrite > lt_O_to_div_times
188         [apply (trans_le ? (pred a))
189           [apply le_prim_n2.
190            apply le_S_S_to_le.
191            apply (lt_times_to_lt 2)
192             [apply le_n_Sn
193             |apply le_S_S_to_le.
194              rewrite < Hcut.
195              apply le_S_S.
196              assumption
197             ]
198           |apply le_pred.
199            apply le_n_Sn
200           ]
201         |apply lt_O_S
202         ]
203       |apply le_S_S.
204        apply not_lt_to_le.intro.
205        apply (le_to_not_lt ? ? H).
206        rewrite > Hcut.
207        lapply (le_S_S_to_le ? ? H3) as H4.
208        apply (le_n_O_elim ? H4).
209        apply leb_true_to_le.reflexivity
210       ]
211     |rewrite > times_SSO.
212      rewrite > S_pred
213       [apply eq_f.assumption
214       |apply (ltn_to_ltO ? ? H)
215       ]
216     ]
217   ]
218 qed.   
219
220 (* This is chebishev psi function *)
221 definition A: nat \to nat \def
222 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
223
224 theorem le_Al1: \forall n.
225 A n \le pi_p (S n) primeb (\lambda p.n).
226 intro.unfold A.
227 cases n
228   [simplify.apply le_n
229   |apply le_pi_p.
230    intros.
231    apply le_exp_log.
232    apply lt_O_S
233   ]
234 qed.
235
236 theorem le_Al: \forall n.
237 A n \le exp n (prim n).
238 intro.unfold prim.
239 rewrite < exp_sigma_p.
240 apply le_Al1.
241 qed.
242
243 theorem leA_r2: \forall n.
244 exp n (prim n) \le A n * A n.
245 intro.unfold prim.
246 elim (le_to_or_lt_eq ? ? (le_O_n n))
247   [rewrite < (exp_sigma_p (S n) n primeb).
248    unfold A.
249    rewrite < times_pi_p.
250    apply le_pi_p.
251    intros.
252    rewrite < exp_plus_times.
253    apply (trans_le ? (exp i (S(log i n))))
254     [apply lt_to_le.
255      apply lt_exp_log.
256      apply prime_to_lt_SO.
257      apply primeb_true_to_prime.
258      assumption
259     |apply le_exp
260       [apply prime_to_lt_O.
261        apply primeb_true_to_prime.
262        assumption
263       |rewrite > plus_n_O.
264        simplify.
265        rewrite > plus_n_Sm.
266        apply le_plus_r.
267        apply lt_O_log
268         [assumption
269         |apply le_S_S_to_le.
270          apply H1
271         ]
272       ]
273     ]
274   |rewrite < H. apply le_n
275   ]
276 qed.
277
278 (* an equivalent formulation for psi *)
279 definition A': nat \to nat \def
280 \lambda n. pi_p (S n) primeb 
281   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
282
283 theorem eq_A_A': \forall n.A n = A' n.
284 intro.unfold A.unfold A'.
285 apply eq_pi_p
286   [intros.reflexivity
287   |intros.
288    apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
289     [apply eq_f.apply sym_eq.apply sigma_p_true
290     |apply sym_eq.apply exp_sigma_p
291     ]
292   ]
293 qed.
294
295 theorem eq_pi_p_primeb_divides_b: \forall n,m.
296 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
297 = pi_p n primeb (\lambda p.exp p (ord m p)).
298 intro.
299 elim n
300   [reflexivity
301   |apply (bool_elim ? (primeb n1));intro
302     [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
303       [apply (bool_elim ? (divides_b n1 m));intro
304         [rewrite > true_to_pi_p_Sn
305           [apply eq_f.
306            apply H
307           |apply true_to_true_to_andb_true;assumption
308           ]
309         |rewrite > false_to_pi_p_Sn
310           [rewrite > not_divides_to_ord_O
311             [simplify in ⊢ (? ? ? (? % ?)).
312              rewrite > sym_times.
313              rewrite < times_n_SO.
314              apply H
315             |apply primeb_true_to_prime.assumption
316             |apply divides_b_false_to_not_divides.
317              assumption
318             ]
319           |rewrite > H1.rewrite > H2.reflexivity
320           ]
321         ]
322       |assumption
323       ]
324     |rewrite > false_to_pi_p_Sn
325       [rewrite > false_to_pi_p_Sn
326         [apply H
327         |assumption
328         ]
329       |rewrite > H1.reflexivity
330       ]
331     ]
332   ]
333 qed.
334
335 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
336 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
337 intro.elim q
338   [apply False_ind.
339    apply (not_le_Sn_O ? H1)
340   |apply (bool_elim ? (primeb n∧divides_b n m));intro
341     [rewrite > true_to_pi_p_Sn
342       [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
343         [apply eq_f.
344          rewrite > (H (ord_rem m n))
345           [apply eq_pi_p1
346             [intros.
347              apply (bool_elim ? (primeb x));intro
348               [simplify.
349                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
350                 [apply sym_eq.
351                  apply divides_to_divides_b_true
352                   [apply prime_to_lt_O.
353                    apply primeb_true_to_prime.
354                    assumption
355                   |apply (trans_divides ? (ord_rem m n))
356                     [apply divides_b_true_to_divides.
357                      assumption
358                     |apply divides_ord_rem
359                       [apply (trans_lt ? x)
360                         [apply prime_to_lt_SO.
361                          apply primeb_true_to_prime.
362                          assumption
363                         |assumption
364                         ]
365                       |assumption
366                       ]
367                     ]
368                   ]
369                 |apply sym_eq.
370                  apply not_divides_to_divides_b_false
371                   [apply prime_to_lt_O.
372                    apply primeb_true_to_prime.
373                    assumption
374                   |apply ord_O_to_not_divides
375                     [assumption
376                     |apply primeb_true_to_prime.
377                      assumption
378                     |rewrite < (ord_ord_rem n)
379                       [apply not_divides_to_ord_O
380                         [apply primeb_true_to_prime.
381                          assumption
382                         |apply divides_b_false_to_not_divides.
383                          assumption
384                         ]
385                       |assumption
386                       |apply primeb_true_to_prime.
387                        apply (andb_true_true ? ? H3)
388                       |apply primeb_true_to_prime.
389                        assumption
390                       |assumption
391                       ]
392                     ]
393                   ]
394                 ]
395               |reflexivity
396               ]
397             |intros.
398              apply eq_f.
399              apply ord_ord_rem
400               [assumption
401               |apply primeb_true_to_prime.
402                apply (andb_true_true ? ? H3)
403               |apply primeb_true_to_prime.
404                apply (andb_true_true ? ? H5)
405               |assumption
406               ]
407             ]
408           |apply lt_O_ord_rem
409             [apply prime_to_lt_SO.
410              apply primeb_true_to_prime.
411              apply (andb_true_true ? ? H3)
412             |assumption
413             ]
414           |apply not_eq_to_le_to_lt
415             [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
416               [elim H4.
417                intro.rewrite > H7 in H6.simplify in H6.
418                apply (not_divides_ord_rem m n)
419                 [assumption
420                 |apply prime_to_lt_SO.
421                  apply primeb_true_to_prime.
422                  apply (andb_true_true ? ? H3)
423                 |apply divides_b_true_to_divides.
424                  apply (andb_true_true_r ? ? H6)
425                 ]
426               |elim H4.rewrite > H6.
427                apply lt_to_not_eq.
428                apply prime_to_lt_O.
429                apply primeb_true_to_prime.
430                apply (andb_true_true ? ? H3)
431               ]
432             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
433               [apply le_to_le_max.
434                apply divides_to_le
435                 [assumption
436                 |apply divides_ord_rem
437                   [apply prime_to_lt_SO.
438                    apply primeb_true_to_prime.
439                    apply (andb_true_true ? ? H3)
440                   |assumption
441                   ]
442                 ]
443               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
444                 [apply le_max_f_max_g.
445                  intros.
446                  apply (bool_elim ? (primeb i));intro
447                   [simplify.
448                    apply divides_to_divides_b_true
449                     [apply prime_to_lt_O.
450                      apply primeb_true_to_prime.
451                      assumption
452                     |apply (trans_divides ? (ord_rem m n))
453                       [apply divides_b_true_to_divides.
454                        apply (andb_true_true_r ? ? H5)
455                       |apply divides_ord_rem
456                         [apply prime_to_lt_SO.
457                          apply primeb_true_to_prime.
458                          apply (andb_true_true ? ? H3)
459                         |assumption
460                         ]
461                       ]
462                     ]
463                   |rewrite > H6 in H5.
464                    assumption
465                   ]
466                 |apply le_S_S_to_le.
467                  assumption
468                 ]
469               ]
470             ]
471           ]
472         |apply prime_to_lt_SO.
473          apply primeb_true_to_prime.
474          apply (andb_true_true ? ? H3)
475         |assumption
476         ]
477       |assumption
478       ]
479     |elim (le_to_or_lt_eq ? ? H1)
480       [rewrite > false_to_pi_p_Sn
481         [apply H
482           [assumption
483           |apply false_to_lt_max
484             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
485               [apply lt_to_le.
486                apply lt_SO_max_prime.
487                assumption
488               |apply le_S_S_to_le.
489                assumption
490               ]
491             |assumption
492             |apply le_S_S_to_le.
493              assumption
494             ]
495           ]
496         |assumption
497         ]
498       |rewrite < H4.
499        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
500        apply eq_pi_p
501         [intros.
502          apply (bool_elim ? (primeb x));intro
503           [apply sym_eq.
504            change with (divides_b x (S O) =false).
505            apply not_divides_to_divides_b_false
506             [apply prime_to_lt_O.
507              apply primeb_true_to_prime.
508              assumption
509             |intro.
510              apply (le_to_not_lt x (S O))
511               [apply divides_to_le
512                 [apply lt_O_S.assumption
513                 |assumption
514                 ]
515               |elim (primeb_true_to_prime ? H6).
516                assumption
517               ]
518             ]
519           |reflexivity
520           ]
521         |intros.reflexivity
522         ]
523       ]
524     ]
525   ]
526 qed.
527
528 (* factorization of n into primes *)
529 theorem pi_p_primeb_divides_b: \forall n. O < n \to 
530 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
531 intros.
532 apply lt_max_to_pi_p_primeb
533   [assumption
534   |apply le_S_S.
535    apply le_max_n
536   ]
537 qed.
538
539 theorem pi_p_primeb: \forall n. O < n \to 
540 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
541 intros.
542 rewrite < eq_pi_p_primeb_divides_b.
543 apply pi_p_primeb_divides_b.
544 assumption.
545 qed.
546
547 theorem le_ord_log: \forall n,p. O < n \to 1 < p \to
548 ord n p \le log p n.
549 intros.
550 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
551   [rewrite > log_exp
552     [apply le_plus_n_r
553     |assumption
554     |apply lt_O_ord_rem;assumption
555     ]
556   |assumption
557   |assumption
558   ]
559 qed.
560
561 theorem sigma_p_divides_b:
562 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
563 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
564 intro.elim m
565   [reflexivity
566   |simplify in ⊢ (? ? ? (? % ? ?)).
567    rewrite > true_to_sigma_p_Sn
568     [rewrite > sym_plus.rewrite < plus_n_SO.
569      apply eq_f.
570      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
571      apply eq_sigma_p1
572       [intros.
573        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
574         [apply sym_eq.
575          apply divides_to_divides_b_true
576           [apply lt_O_exp.
577            apply prime_to_lt_O.
578            assumption
579           |apply (witness ? ? ((exp p (n - x))*n1)).
580            rewrite < assoc_times.
581            rewrite < exp_plus_times.
582            apply eq_f2
583             [apply eq_f.simplify.
584              apply eq_f.
585              rewrite > sym_plus.
586              apply plus_minus_m_m.
587              apply lt_to_le.assumption
588             |reflexivity
589             ]
590           ]
591         |apply sym_eq.
592          apply False_ind.
593          apply (divides_b_false_to_not_divides ? ? H5).
594          apply (witness ? ? ((exp p (n - S x))*n1)).
595          rewrite < assoc_times.
596          rewrite < exp_plus_times.
597          apply eq_f2
598           [apply eq_f.
599            rewrite > sym_plus.
600            apply plus_minus_m_m.
601            assumption
602           |reflexivity
603           ]
604         ]
605       |intros.reflexivity
606       ]
607     |apply divides_to_divides_b_true
608       [apply lt_O_exp.
609        apply prime_to_lt_O.assumption
610       |apply (witness ? ? n1).reflexivity
611       ]
612     ]
613   ]
614 qed.
615   
616 theorem sigma_p_divides_b1:
617 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
618 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
619 intros.
620 lapply (prime_to_lt_SO ? H1) as H4.
621 lapply (prime_to_lt_O ? H1) as H5.
622 rewrite > (false_to_eq_sigma_p m k)
623   [apply sigma_p_divides_b;assumption
624   |assumption
625   |intros.
626    apply not_divides_to_divides_b_false
627     [apply lt_O_exp.assumption
628     |intro.apply (le_to_not_lt ? ? H6).
629      unfold lt.
630      rewrite < (ord_exp p)
631       [rewrite > (plus_n_O m).
632        rewrite < (not_divides_to_ord_O ? ? H1 H2).
633        rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
634        rewrite < ord_times
635         [apply divides_to_le_ord
636           [apply lt_O_exp.assumption
637           |rewrite > (times_n_O O).
638            apply lt_times
639             [apply lt_O_exp.assumption
640             |assumption
641             ]
642           |assumption
643           |assumption
644           ]
645         |apply lt_O_exp.assumption
646         |assumption
647         |assumption
648         ]
649       |assumption
650       ]
651     ]
652   ]
653 qed.
654
655 theorem eq_ord_sigma_p:
656 \forall n,m,x. O < n \to prime x \to 
657 exp x m \le n \to n < exp x (S m) \to
658 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.1).
659 intros.
660 lapply (prime_to_lt_SO ? H1).
661 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
662   [apply sigma_p_divides_b1
663     [apply lt_O_ord_rem;assumption
664     |assumption
665     |apply not_divides_ord_rem;assumption
666     |apply lt_S_to_le.
667      apply (le_to_lt_to_lt ? (log x n))
668       [apply le_ord_log;assumption
669       |apply (lt_exp_to_lt x)
670         [assumption
671         |apply (le_to_lt_to_lt ? n ? ? H3).
672          apply le_exp_log.
673          assumption
674         ]
675       ]
676     ]
677   |assumption
678   |assumption
679   ]
680 qed.
681     
682 theorem pi_p_primeb1: \forall n. O < n \to 
683 n = pi_p (S n) primeb 
684   (\lambda p.(pi_p (log p n) 
685     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
686 intros.
687 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
688 apply eq_pi_p1
689   [intros.reflexivity
690   |intros.
691    rewrite > exp_sigma_p.
692    apply eq_f.
693    apply eq_ord_sigma_p
694     [assumption
695     |apply primeb_true_to_prime.
696      assumption
697     |apply le_exp_log.assumption
698     |apply lt_exp_log.
699      apply prime_to_lt_SO.
700      apply primeb_true_to_prime.
701      assumption
702     ]
703   ]
704 qed.
705
706 (* the factorial function *)
707 theorem eq_fact_pi_p:\forall n. fact n = 
708 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
709 intro.elim n
710   [reflexivity
711   |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
712    rewrite > true_to_pi_p_Sn
713     [apply eq_f.assumption
714     |reflexivity
715     ]
716   ]
717 qed.
718    
719 theorem eq_sigma_p_div: \forall n,q.O < q \to
720 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
721 =n/q.
722 intros.
723 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
724   [apply div_mod_spec_intro
725     [apply lt_mod_m_m.assumption
726     |elim n
727       [simplify.elim q;reflexivity
728       |elim (or_div_mod1 n1 q)
729         [elim H2.clear H2.
730          rewrite > divides_to_mod_O
731           [rewrite < plus_n_O.
732            rewrite > true_to_sigma_p_Sn
733             [rewrite > H4 in ⊢ (? ? % ?).
734              apply eq_f2
735               [rewrite < sym_plus.
736                rewrite < plus_n_SO.
737                apply eq_f.
738                apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
739                 [apply div_mod_spec_div_mod.
740                  assumption
741                 |apply div_mod_spec_intro
742                   [apply lt_mod_m_m.assumption
743                   |assumption
744                   ]
745                 ]
746               |reflexivity
747               ]
748             |apply true_to_true_to_andb_true
749               [reflexivity
750               |apply divides_to_divides_b_true;assumption
751               ]
752             ]
753           |assumption
754           |assumption
755           ]
756         |elim H2.clear H2.
757          rewrite > false_to_sigma_p_Sn
758           [rewrite > mod_S
759             [rewrite < plus_n_Sm.
760              apply eq_f.
761              assumption
762             |assumption
763             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
764               [assumption
765               |apply False_ind.
766                apply H3.
767                apply (witness ? ? (S(div n1 q))).
768                rewrite < times_n_Sm.
769                rewrite < sym_plus.
770                rewrite < H2 in ⊢ (? ? ? (? ? %)).
771                rewrite > sym_times.
772                assumption
773               |apply lt_mod_m_m.
774                assumption
775               ]
776             ]
777           |rewrite > not_divides_to_divides_b_false
778             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
779             |assumption
780             |assumption
781             ]
782           ]
783         |assumption
784         ]
785       ]
786     ]
787   |apply div_mod_spec_div_mod.
788    assumption
789   ]
790 qed.              
791
792 (* still another characterization of the factorial *)
793 theorem fact_pi_p: \forall n. fact n =
794 pi_p (S n) primeb 
795   (\lambda p.(pi_p (log p n) 
796     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
797 intros.
798 rewrite > eq_fact_pi_p.
799 apply (trans_eq ? ? 
800   (pi_p (S n) (λm:nat.leb (S O) m) 
801    (λm.pi_p (S m) primeb 
802     (\lambda p.(pi_p (log p m) 
803      (\lambda i.divides_b (exp p (S i)) m) (\lambda i.p))))))
804   [apply eq_pi_p1;intros
805     [reflexivity
806     |apply pi_p_primeb1.
807      apply leb_true_to_le.assumption
808     ]
809   |apply (trans_eq ? ? 
810     (pi_p (S n) (λm:nat.leb (S O) m)
811      (λm:nat
812       .pi_p (S m) (\lambda p.primeb p\land leb p m)
813        (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
814     [apply eq_pi_p1
815       [intros.reflexivity
816       |intros.apply eq_pi_p1
817         [intros.elim (primeb x1)
818           [simplify.apply sym_eq.
819            apply le_to_leb_true.
820            apply le_S_S_to_le.
821            assumption
822           |reflexivity
823           ]
824         |intros.reflexivity
825         ]
826       ]
827     |apply (trans_eq ? ? 
828       (pi_p (S n) (λm:nat.leb (S O) m)
829        (λm:nat
830         .pi_p (S n) (λp:nat.primeb p∧leb p m)
831          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
832       [apply eq_pi_p1
833         [intros.reflexivity
834         |intros.
835          apply sym_eq.
836          apply false_to_eq_pi_p
837           [assumption
838           |intros.rewrite > lt_to_leb_false
839             [elim primeb;reflexivity|assumption]
840           ]
841         ]
842       |(* make a general theorem *)
843        apply (trans_eq ? ? 
844         (pi_p (S n) primeb
845          (λp:nat
846           .pi_p (S n) (λm.leb p m)
847            (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
848         ))
849         [apply pi_p_pi_p1.
850          intros.
851          apply (bool_elim ? (primeb y \land leb y x));intros
852           [rewrite > (le_to_leb_true (S O) x)
853             [reflexivity
854             |apply (trans_le ? y)
855               [apply prime_to_lt_O.
856                apply primeb_true_to_prime.
857                apply (andb_true_true ? ? H2)
858               |apply leb_true_to_le.
859                apply (andb_true_true_r ? ? H2)
860               ]
861             ]
862           |elim (leb (S O) x);reflexivity
863           ]
864         |apply eq_pi_p1
865           [intros.reflexivity
866           |intros.
867            apply (trans_eq ? ? 
868             (pi_p (S n) (λm:nat.leb x m)
869              (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
870             [apply eq_pi_p1
871               [intros.reflexivity
872               |intros.
873                apply sym_eq.
874                apply false_to_eq_pi_p
875                 [apply le_log
876                   [apply prime_to_lt_SO.
877                    apply primeb_true_to_prime.
878                    assumption
879                   |apply le_S_S_to_le.
880                    assumption
881                   ]
882                 |intros.
883                  apply not_divides_to_divides_b_false
884                   [apply lt_O_exp.
885                    apply prime_to_lt_O.
886                    apply primeb_true_to_prime.
887                    assumption
888                   |intro.
889                    apply (lt_to_not_le x1 (exp x (S i)))
890                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
891                       [apply lt_exp_log.
892                        apply prime_to_lt_SO.
893                        apply primeb_true_to_prime.
894                        assumption
895                       |apply le_exp
896                         [apply prime_to_lt_O.
897                          apply primeb_true_to_prime.
898                          assumption
899                         |apply le_S_S.
900                          assumption
901                         ]
902                       ]
903                     |apply divides_to_le
904                       [apply (lt_to_le_to_lt ? x)
905                         [apply prime_to_lt_O.
906                          apply primeb_true_to_prime.
907                          assumption
908                         |apply leb_true_to_le.
909                          assumption
910                         ]
911                       |assumption
912                       ]
913                     ]
914                   ]
915                 ]
916               ]
917             |apply 
918              (trans_eq ? ? 
919               (pi_p (log x n) (λi:nat.true)
920                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
921               [apply (pi_p_pi_p1 (\lambda m,i.x)).
922                intros.
923                reflexivity
924               |apply eq_pi_p1
925                 [intros.reflexivity
926                 |intros.
927                  rewrite > exp_sigma_p.
928                  apply eq_f.
929                  apply (trans_eq ? ? 
930                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
931                   [apply eq_sigma_p1
932                     [intros.
933                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
934                       [apply (bool_elim ? (leb x x2));intro
935                         [rewrite > le_to_leb_true
936                           [reflexivity
937                           |apply (trans_le ? x)
938                             [apply prime_to_lt_O.
939                              apply primeb_true_to_prime.
940                              assumption
941                             |apply leb_true_to_le.
942                              assumption
943                             ]
944                           ]
945                         |rewrite > lt_to_leb_false
946                           [reflexivity
947                           |apply not_le_to_lt.intro.
948                            apply (leb_false_to_not_le ? ? H6).
949                            apply (trans_le ? (exp x (S x1)))
950                             [rewrite > times_n_SO in ⊢ (? % ?).
951                              change with (exp x (S O) \le exp x (S x1)).
952                              apply le_exp
953                               [apply prime_to_lt_O.
954                                apply primeb_true_to_prime.
955                                assumption
956                               |apply le_S_S.apply le_O_n.
957                               ]
958                             |apply divides_to_le
959                               [assumption
960                               |apply divides_b_true_to_divides.
961                                assumption
962                               ]
963                             ]
964                           ]
965                         ]
966                       |rewrite < andb_sym.
967                        rewrite < andb_sym in ⊢ (? ? ? %).
968                        reflexivity
969                       ]
970                     |intros.reflexivity
971                     ]
972                   |apply eq_sigma_p_div.
973                    apply lt_O_exp.
974                    apply prime_to_lt_O.
975                    apply primeb_true_to_prime.
976                    assumption
977                   ]
978                 ]
979               ]
980             ]
981           ]
982         ]
983       ]
984     ]
985   ]
986 qed.
987
988 (* odd n is just mod n (S(S O)) 
989 let rec odd n \def
990   match n with 
991   [ O \Rightarrow O
992   | S m \Rightarrow (S O) - odd m 
993   ].
994
995 theorem le_odd_SO: \forall n. odd n \le S O.
996 intro.elim n
997   [apply le_O_n
998   |simplify.cases (odd n1)
999     [simplify.apply le_n.
1000     |apply le_O_n
1001     ]
1002   ]
1003 qed.
1004
1005 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
1006 intro.elim n
1007   [apply (lt_O_n_elim ? H).
1008    intro.simplify.reflexivity
1009   |
1010 *)
1011
1012 theorem fact_pi_p2: \forall n. fact (2*n) =
1013 pi_p (S (2*n)) primeb 
1014   (\lambda p.(pi_p (log p (2*n)) 
1015     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))))).
1016 intros.rewrite > fact_pi_p.
1017 apply eq_pi_p1
1018   [intros.reflexivity
1019   |intros.apply eq_pi_p
1020     [intros.reflexivity
1021     |intros.
1022      rewrite < exp_plus_times.
1023      apply eq_f.
1024      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
1025      apply SSO_mod.
1026      apply lt_O_exp.
1027      apply prime_to_lt_O.
1028      apply primeb_true_to_prime.
1029      assumption
1030     ]
1031   ]
1032 qed.
1033
1034 theorem fact_pi_p3: \forall n. fact (2*n) =
1035 pi_p (S (2*n)) primeb 
1036   (\lambda p.(pi_p (log p (2*n)) 
1037     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))*
1038 pi_p (S (2*n)) primeb 
1039   (\lambda p.(pi_p (log p (2*n))   
1040     (\lambda i.true) (\lambda i.(exp p (mod (2*n /(exp p (S i))) 2))))).
1041 intros.
1042 rewrite < times_pi_p.
1043 rewrite > fact_pi_p2.
1044 apply eq_pi_p;intros 
1045   [reflexivity
1046   |apply times_pi_p
1047   ]
1048 qed.
1049
1050 theorem pi_p_primeb4: \forall n. 1 < n \to
1051 pi_p (S (2*n)) primeb 
1052   (\lambda p.(pi_p (log p (2*n)) 
1053     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
1054
1055 pi_p (S n) primeb 
1056   (\lambda p.(pi_p (log p (2*n)) 
1057     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
1058 intros.
1059 apply or_false_eq_SO_to_eq_pi_p
1060   [apply le_S_S.
1061    apply le_times_n.
1062    apply lt_O_S
1063   |intros.
1064    right.
1065    rewrite > log_i_SSOn
1066     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
1067      rewrite < times_n_SO.
1068      rewrite > eq_div_O
1069       [reflexivity
1070       |simplify.rewrite < times_n_SO.assumption
1071       ]
1072     |assumption
1073     |assumption
1074     |apply le_S_S_to_le.assumption
1075     ]
1076   ]
1077 qed.
1078    
1079 theorem pi_p_primeb5: \forall n. 1 < n \to
1080 pi_p (S (2*n)) primeb 
1081   (\lambda p.(pi_p (log p ((S(S O))*n)) 
1082     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
1083
1084 pi_p (S n) primeb 
1085   (\lambda p.(pi_p (log p n) 
1086     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
1087 intros.
1088 rewrite > (pi_p_primeb4 ? H).
1089 apply eq_pi_p1;intros
1090   [reflexivity
1091   |apply or_false_eq_SO_to_eq_pi_p
1092     [apply le_log
1093       [apply prime_to_lt_SO.
1094        apply primeb_true_to_prime.
1095        assumption
1096       |apply le_times_n.
1097        apply lt_O_S
1098       ]
1099     |intros.right.
1100      rewrite > eq_div_O
1101       [simplify.reflexivity
1102       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
1103         [apply lt_exp_log.
1104          apply prime_to_lt_SO.
1105          apply primeb_true_to_prime.
1106          assumption
1107         |apply le_exp
1108           [apply prime_to_lt_O.
1109            apply primeb_true_to_prime.
1110            assumption
1111           |apply le_S_S.
1112            assumption
1113           ]
1114         ]
1115       ]
1116     ]
1117   ]
1118 qed.
1119
1120 theorem exp_fact_SSO: \forall n.
1121 exp (fact n) 2
1122
1123 pi_p (S n) primeb 
1124   (\lambda p.(pi_p (log p n) 
1125     (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
1126 intros.
1127 rewrite > fact_pi_p.
1128 rewrite < exp_pi_p.
1129 apply eq_pi_p;intros
1130   [reflexivity
1131   |apply sym_eq.
1132    apply exp_times_pi_p
1133   ]
1134 qed.
1135
1136 definition B \def
1137 \lambda n.
1138 pi_p (S n) primeb 
1139   (\lambda p.(pi_p (log p n)   
1140     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
1141
1142 theorem B_SSSO: B 3 = 6.
1143 reflexivity.
1144 qed.
1145
1146 theorem B_SSSSO: B 4 = 6.
1147 reflexivity.
1148 qed.
1149
1150 theorem B_SSSSSO: B 5 = 30.
1151 reflexivity.
1152 qed.
1153
1154 theorem B_SSSSSSO: B 6 = 20.
1155 reflexivity.
1156 qed.
1157
1158 theorem B_SSSSSSSO: B 7 = 140.
1159 reflexivity.
1160 qed.
1161
1162 theorem B_SSSSSSSSO: B 8 = 70.
1163 reflexivity.
1164 qed.
1165
1166 theorem eq_fact_B:\forall n.S O < n \to
1167 fact (2*n) = exp (fact n) 2 * B(2*n).
1168 intros. unfold B.
1169 rewrite > fact_pi_p3.
1170 apply eq_f2
1171   [apply sym_eq.
1172    rewrite > pi_p_primeb5
1173     [apply exp_fact_SSO
1174     |assumption
1175     ]
1176   |reflexivity
1177   ]
1178 qed.
1179
1180 theorem le_B_A: \forall n. B n \le A n.
1181 intro.unfold B.
1182 rewrite > eq_A_A'.
1183 unfold A'.
1184 apply le_pi_p.intros.
1185 apply le_pi_p.intros.
1186 rewrite > exp_n_SO in ⊢ (? ? %).
1187 apply le_exp
1188   [apply prime_to_lt_O.
1189    apply primeb_true_to_prime.
1190    assumption
1191   |apply le_S_S_to_le.
1192    apply lt_mod_m_m.
1193    apply lt_O_S
1194   ]
1195 qed.
1196
1197 theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n).
1198 intros.unfold B.
1199 rewrite > eq_A_A'.
1200 unfold A'.
1201 cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
1202   [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
1203     [rewrite > (pi_p_gi ? ? (S(S O)))
1204       [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
1205         [rewrite < assoc_times.
1206          apply le_times
1207           [rewrite > (pi_p_gi ? ? O)
1208             [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
1209               [rewrite < assoc_times.
1210                apply le_times
1211                 [rewrite < exp_n_SO.
1212                  change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
1213                  with ((S(S O))*(S(S O))).
1214                  rewrite > assoc_times.
1215                  rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
1216                  rewrite > lt_O_to_div_times
1217                   [rewrite > divides_to_mod_O
1218                     [apply le_n
1219                     |apply lt_O_S
1220                     |apply (witness ? ? n).reflexivity
1221                     ]
1222                   |apply lt_O_S
1223                   ]
1224                 |apply le_pi_p.intros.
1225                  rewrite > exp_n_SO in ⊢ (? ? %).
1226                  apply le_exp
1227                   [apply lt_O_S
1228                   |apply le_S_S_to_le.
1229                    apply lt_mod_m_m.
1230                    apply lt_O_S
1231                   ]
1232                 ]
1233               |assumption
1234               |reflexivity
1235               ]
1236             |assumption
1237             |reflexivity
1238             ]
1239           |apply le_pi_p.intros.
1240            apply le_pi_p.intros.
1241            rewrite > exp_n_SO in ⊢ (? ? %).
1242            apply le_exp
1243             [apply prime_to_lt_O.
1244              apply primeb_true_to_prime.
1245              apply (andb_true_true ? ? H2)
1246             |apply le_S_S_to_le.
1247              apply lt_mod_m_m.
1248              apply lt_O_S
1249             ]
1250           ]
1251         |assumption
1252         |reflexivity
1253         ]
1254       |assumption
1255       |reflexivity
1256       ]
1257     |apply lt_O_log
1258       [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
1259        apply lt_times_r1
1260         [apply lt_O_S
1261         |assumption
1262         ]
1263       |rewrite > times_n_SO in ⊢ (? % ?).
1264        apply le_times
1265         [apply le_S.apply le_S.apply le_n
1266         |assumption
1267         ]
1268       ]
1269     ]
1270   |apply le_S_S.
1271    rewrite > times_n_SO in ⊢ (? % ?).
1272    apply le_times
1273     [apply le_S.apply le_n_Sn
1274     |assumption
1275     ]
1276   ]
1277 qed.
1278
1279 (* not usefull    
1280 theorem le_fact_A:\forall n.S O < n \to
1281 fact (2*n) \le exp (fact n) 2 * A (2*n).
1282 intros.
1283 rewrite > eq_fact_B
1284   [apply le_times_r.
1285    apply le_B_A
1286   |assumption
1287   ]
1288 qed. *)
1289
1290 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1291 B (2*n) \le exp 2 (pred (2*n)).
1292 intros.
1293 apply (le_times_to_le (exp (fact n) (S(S O))))
1294   [apply lt_O_exp.
1295    apply lt_O_fact
1296   |rewrite < eq_fact_B
1297     [rewrite < sym_times in ⊢ (? ? %).
1298      rewrite > exp_SSO.
1299      rewrite < assoc_times.
1300      apply fact1
1301     |assumption
1302     ]
1303   ]
1304 qed.
1305
1306 theorem le_B_exp: \forall n.
1307 B (2*n) \le exp 2 (pred (2*n)).
1308 intro.cases n
1309   [apply le_n
1310   |cases n1
1311     [simplify.apply le_n
1312     |apply lt_SO_to_le_B_exp.
1313      apply le_S_S.apply lt_O_S.
1314     ]
1315   ]
1316 qed.
1317
1318 theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
1319 B (2*n) \le exp 2 ((2*n)-2).
1320 intros.
1321 apply (le_times_to_le (exp (fact n) (S(S O))))
1322   [apply lt_O_exp.
1323    apply lt_O_fact
1324   |rewrite < eq_fact_B
1325     [rewrite < sym_times in ⊢ (? ? %).
1326      rewrite > exp_SSO.
1327      rewrite < assoc_times.
1328      apply lt_SSSSO_to_fact.assumption
1329     |apply lt_to_le.apply lt_to_le.
1330      apply lt_to_le.assumption
1331     ]
1332   ]
1333 qed.
1334
1335 theorem lt_SO_to_le_exp_B: \forall n. 1 < n \to
1336 exp 2 (2*n) \le 2 * n * B (2*n).
1337 intros.
1338 apply (le_times_to_le (exp (fact n) (S(S O))))
1339   [apply lt_O_exp.
1340    apply lt_O_fact
1341   |rewrite < assoc_times in ⊢ (? ? %).
1342    rewrite > sym_times in ⊢ (? ? (? % ?)).
1343    rewrite > assoc_times in ⊢ (? ? %).
1344    rewrite < eq_fact_B
1345     [rewrite < sym_times.
1346      apply fact3.
1347      apply lt_to_le.assumption
1348     |assumption
1349     ]
1350   ]
1351 qed.
1352
1353 theorem le_exp_B: \forall n. O < n \to
1354 exp 2 (2*n) \le 2 * n * B (2*n).
1355 intros.
1356 elim H
1357   [apply le_n
1358   |apply lt_SO_to_le_exp_B.
1359    apply le_S_S.assumption
1360   ]
1361 qed.
1362
1363 theorem eq_A_SSO_n: \forall n.O < n \to
1364 A(2*n) =
1365  pi_p (S (2*n)) primeb 
1366   (\lambda p.(pi_p (log p (2*n) )   
1367     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1368  *A n.
1369 intro.
1370 rewrite > eq_A_A'.rewrite > eq_A_A'.
1371 unfold A'.intros.
1372 cut (
1373  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1374  = pi_p (S ((S(S O))*n)) primeb
1375     (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
1376   [rewrite > Hcut.
1377    rewrite < times_pi_p.
1378    apply eq_pi_p1;intros
1379     [reflexivity
1380     |rewrite < times_pi_p.
1381      apply eq_pi_p;intros
1382       [reflexivity
1383       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1384         [simplify.rewrite < times_n_SO.apply times_n_SO
1385         |simplify.rewrite < plus_n_O.apply times_n_SO
1386         ]
1387       ]
1388     ]
1389   |apply (trans_eq ? ? (pi_p (S n) primeb 
1390     (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
1391     [apply eq_pi_p1;intros
1392       [reflexivity
1393       |apply eq_pi_p1;intros
1394         [reflexivity
1395         |rewrite > lt_to_leb_false
1396           [simplify.apply times_n_SO
1397           |apply le_S_S.
1398            apply (trans_le ? (exp x (log x n)))
1399             [apply le_exp
1400               [apply prime_to_lt_O.
1401                apply primeb_true_to_prime.
1402                assumption
1403               |assumption
1404               ]
1405             |apply le_exp_log.
1406              assumption
1407             ]
1408           ]
1409         ]
1410       ]
1411     |apply (trans_eq ? ? 
1412       (pi_p (S ((S(S O))*n)) primeb
1413        (λp:nat.pi_p (log p n) (λi:nat.true)
1414         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1415       [apply sym_eq.
1416        apply or_false_eq_SO_to_eq_pi_p
1417         [apply le_S_S.
1418          simplify.
1419          apply le_plus_n_r
1420         |intros.right.
1421          rewrite > lt_to_log_O
1422           [reflexivity
1423           |assumption
1424           |assumption
1425           ]
1426         ]
1427       |apply eq_pi_p1;intros
1428         [reflexivity
1429         |apply sym_eq.
1430          apply or_false_eq_SO_to_eq_pi_p
1431           [apply le_log
1432             [apply prime_to_lt_SO.
1433              apply primeb_true_to_prime.
1434              assumption
1435             |simplify.
1436              apply le_plus_n_r
1437             ]
1438           |intros.right.
1439            rewrite > le_to_leb_true
1440             [simplify.reflexivity
1441             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1442               [apply lt_exp_log.
1443                apply prime_to_lt_SO.
1444                apply primeb_true_to_prime.
1445                assumption
1446               |apply le_exp
1447                 [apply prime_to_lt_O.
1448                  apply primeb_true_to_prime.
1449                  assumption
1450                 |apply le_S_S.assumption
1451                 ]
1452               ]
1453             ]
1454           ]
1455         ]
1456       ]
1457     ]
1458   ]
1459 qed.
1460                
1461 theorem le_A_BA1: \forall n. O < n \to 
1462 A(2*n) \le B(2*n)*A n.
1463 intros.
1464 rewrite > eq_A_SSO_n
1465   [apply le_times_l.
1466    unfold B.
1467    apply le_pi_p.intros.
1468    apply le_pi_p.intros.
1469    apply le_exp
1470     [apply prime_to_lt_O.
1471      apply primeb_true_to_prime.
1472      assumption
1473     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1474       [simplify in ⊢ (? % ?).
1475        cut ((S(S O))*n/i\sup(S i1) = S O)
1476         [rewrite > Hcut.apply le_n
1477         |apply (div_mod_spec_to_eq 
1478           ((S(S O))*n) (exp i (S i1)) 
1479            ? (mod ((S(S O))*n) (exp i (S i1))) 
1480            ? (minus ((S(S O))*n) (exp i (S i1))) )
1481           [apply div_mod_spec_div_mod.
1482            apply lt_O_exp.
1483            apply prime_to_lt_O.
1484            apply primeb_true_to_prime.
1485            assumption
1486           |cut (i\sup(S i1)≤(S(S O))*n)
1487             [apply div_mod_spec_intro
1488               [apply lt_plus_to_lt_minus
1489                 [assumption
1490                 |simplify in ⊢ (? % ?).
1491                  rewrite < plus_n_O.
1492                  apply lt_plus
1493                   [apply leb_true_to_le.assumption
1494                   |apply leb_true_to_le.assumption
1495                   ]
1496                 ]
1497               |rewrite > sym_plus.
1498                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1499                rewrite < times_n_SO.
1500                apply plus_minus_m_m.
1501                assumption
1502               ]
1503             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1504               [apply le_exp
1505                 [apply prime_to_lt_O.
1506                  apply primeb_true_to_prime.
1507                  assumption
1508                 |assumption
1509                 ]
1510               |apply le_exp_log.
1511                rewrite > (times_n_O O) in ⊢ (? % ?).
1512                apply lt_times 
1513                 [apply lt_O_S
1514                 |assumption
1515                 ]
1516               ]
1517             ]
1518           ]
1519         ]
1520       |apply le_O_n
1521       ]
1522     ]
1523   |assumption
1524   ]
1525 qed.
1526
1527 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1528 intros.cases n
1529   [apply le_n
1530   |apply le_A_BA1.apply lt_O_S
1531   ]
1532 qed.
1533
1534 theorem le_A_exp: \forall n.
1535 A(2*n) \le (exp 2 (pred (2*n)))*A n.
1536 intro.
1537 apply (trans_le ? (B(2*n)*A n))
1538   [apply le_A_BA
1539   |apply le_times_l.
1540    apply le_B_exp
1541   ]
1542 qed.
1543
1544 theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
1545 A(2*n) \le exp 2 ((2*n)-2)*A n.
1546 intros.
1547 apply (trans_le ? (B(2*n)*A n))
1548   [apply le_A_BA
1549   |apply le_times_l.
1550    apply lt_SSSSO_to_le_B_exp.assumption
1551   ]
1552 qed.
1553
1554 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1555 intro.cases n
1556   [apply le_n
1557   |simplify.apply le_plus_r.
1558    apply le_n_Sn
1559   ]
1560 qed.
1561
1562 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1563 intros.
1564 elim H
1565   [apply le_n
1566   |rewrite > times_SSO.
1567    apply le_S_S.
1568    apply (trans_le ? (2*n1))
1569     [assumption
1570     |apply le_n_Sn
1571     ]
1572   ]
1573 qed.
1574
1575 theorem le_A_exp1: \forall n.
1576 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1577 intro.elim n
1578   [simplify.apply le_n
1579   |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1580    apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1581     [apply le_A_exp
1582     |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1583       [apply le_times_r.
1584        assumption
1585       |rewrite < exp_plus_times.
1586        apply le_exp
1587         [apply lt_O_S
1588         |cut (S(S n1) \le 2*(exp 2 n1))
1589           [apply le_S_S_to_le.
1590            change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1591            rewrite < S_pred
1592             [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1593              rewrite < S_pred
1594               [rewrite < eq_minus_plus_plus_minus
1595                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1596                  apply le_n
1597                 |assumption
1598                 ]
1599               |apply lt_to_lt_O_minus.
1600                apply (lt_to_le_to_lt ? (2*(S(S n1))))
1601                 [rewrite > times_n_SO in ⊢ (? % ?).
1602                  rewrite > sym_times.
1603                  apply lt_times_l1
1604                   [apply lt_O_S
1605                   |apply le_n
1606                   ]
1607                 |apply le_times_r.
1608                  assumption
1609                 ]
1610               ]
1611             |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1612              apply le_times
1613               [apply le_n_Sn
1614               |apply lt_O_exp.
1615                apply lt_O_S
1616               ]
1617             ]
1618           |elim n1
1619             [apply le_n
1620             |apply (trans_le ? (2*(S(S n2))))
1621               [apply le_S_times_SSO.
1622                apply lt_O_S
1623               |apply le_times_r.
1624                assumption
1625               ]
1626             ]
1627           ]
1628         ]
1629       ]
1630     ]
1631   ]
1632 qed.
1633
1634 theorem monotonic_A: monotonic nat le A.
1635 unfold.intros.
1636 elim H
1637   [apply le_n
1638   |apply (trans_le ? (A n1))
1639     [assumption
1640     |unfold A.
1641      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1642           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1643       [apply (bool_elim ? (primeb (S n1)));intro
1644         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1645          rewrite > times_n_SO in ⊢ (? % ?).
1646          rewrite > sym_times.
1647          apply le_times
1648           [apply lt_O_exp.apply lt_O_S
1649           |assumption
1650           ]
1651         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1652          assumption
1653         ]
1654       |apply le_pi_p.intros.
1655        apply le_exp
1656         [apply prime_to_lt_O.
1657          apply primeb_true_to_prime.
1658          assumption
1659         |apply le_log
1660           [apply prime_to_lt_SO.
1661            apply primeb_true_to_prime.
1662            assumption
1663           |apply le_S.apply le_n
1664           ]
1665         ]
1666       ]
1667     ]
1668   ]
1669 qed.
1670
1671 (*
1672 theorem le_A_exp2: \forall n. O < n \to
1673 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1674 intros.
1675 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1676   [apply monotonic_A.
1677    apply lt_to_le.
1678    apply lt_exp_log.
1679    apply le_n
1680   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1681     [apply le_A_exp1
1682     |apply le_exp
1683       [apply lt_O_S
1684       |rewrite > assoc_times.apply le_times_r.
1685        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1686        apply le_times_r.
1687        apply le_exp_log.
1688        assumption
1689       ]
1690     ]
1691   ]
1692 qed.
1693 *)
1694
1695 (* example *)
1696 theorem A_SO: A (S O) = S O.
1697 reflexivity.
1698 qed.
1699
1700 theorem A_SSO: A (S(S O)) = S (S O).
1701 reflexivity.
1702 qed.
1703
1704 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1705 reflexivity.
1706 qed.
1707
1708 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1709 reflexivity.
1710 qed.
1711
1712 (*
1713 (* a better result *)
1714 theorem le_A_exp3: \forall n. S O < n \to
1715 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1716 intro.
1717 apply (nat_elim1 n).
1718 intros.
1719 elim (or_eq_eq_S m).
1720 elim H2
1721   [elim (le_to_or_lt_eq (S O) a)
1722     [rewrite > H3 in ⊢ (? % ?).
1723      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1724       [apply le_A_exp
1725       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1726          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1727         [apply le_times_r.
1728          apply H
1729           [rewrite > H3.
1730            rewrite > times_n_SO in ⊢ (? % ?).
1731            rewrite > sym_times.
1732            apply lt_times_l1
1733             [apply lt_to_le.assumption
1734             |apply le_n
1735             ]
1736           |assumption
1737           ]
1738         |rewrite > sym_times.
1739          rewrite > assoc_times.
1740          rewrite < exp_plus_times.
1741          apply (trans_le ? 
1742           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1743           [rewrite > assoc_times.
1744            apply le_times_r.
1745            rewrite < exp_plus_times.
1746            apply le_exp
1747             [apply lt_O_S
1748             |rewrite < H3.
1749              simplify.
1750              rewrite < plus_n_O.
1751              apply le_S.apply le_S.
1752              apply le_n
1753             ]
1754           |apply le_times_l.
1755            rewrite > times_exp.
1756            apply monotonic_exp1.
1757            rewrite > H3.
1758            rewrite > sym_times.
1759            cases a
1760             [apply le_n
1761             |simplify.
1762              rewrite < plus_n_Sm.
1763              apply le_S.
1764              apply le_n
1765             ]
1766           ]
1767         ]
1768       ]
1769     |rewrite < H4 in H3.
1770      simplify in H3.
1771      rewrite > H3.
1772      simplify.
1773      apply le_S_S.apply le_S_S.apply le_O_n
1774     |apply not_lt_to_le.intro.
1775      apply (lt_to_not_le ? ? H1).
1776      rewrite > H3.
1777      apply (le_n_O_elim a)
1778       [apply le_S_S_to_le.assumption
1779       |apply le_O_n
1780       ]
1781     ]
1782   |elim (le_to_or_lt_eq O a (le_O_n ?))
1783     [apply (trans_le ? (A ((S(S O))*(S a))))
1784       [apply monotonic_A.
1785        rewrite > H3.
1786        rewrite > times_SSO.
1787        apply le_n_Sn
1788       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1789         [apply le_A_exp
1790         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1791            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1792           [apply le_times_r.
1793            apply H
1794             [rewrite > H3.
1795              apply le_S_S.
1796              simplify.
1797              rewrite > plus_n_SO.
1798              apply le_plus_r.
1799              rewrite < plus_n_O.
1800              assumption
1801             |apply le_S_S.assumption
1802             ]
1803           |rewrite > sym_times.
1804            rewrite > assoc_times.
1805            rewrite < exp_plus_times.
1806            apply (trans_le ? 
1807             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1808             [rewrite > assoc_times.
1809              apply le_times_r.
1810              rewrite < exp_plus_times.
1811              apply le_exp
1812               [apply lt_O_S
1813               |rewrite > times_SSO.
1814                rewrite < H3.
1815                simplify.
1816                rewrite < plus_n_Sm.
1817                rewrite < plus_n_O.
1818                apply le_n
1819               ]
1820             |apply le_times_l.
1821              rewrite > times_exp.
1822              apply monotonic_exp1.
1823              rewrite > H3.
1824              rewrite > sym_times.
1825              apply le_n
1826             ]
1827           ]
1828         ]
1829       ]
1830     |rewrite < H4 in H3.simplify in H3.
1831      apply False_ind.
1832      apply (lt_to_not_le ? ? H1).
1833      rewrite > H3.
1834      apply le_
1835     ]
1836   ]
1837 qed.
1838 *)
1839
1840 theorem le_A_exp4: \forall n. S O < n \to
1841 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1842 intro.
1843 apply (nat_elim1 n).
1844 intros.
1845 elim (or_eq_eq_S m).
1846 elim H2
1847   [elim (le_to_or_lt_eq (S O) a)
1848     [rewrite > H3 in ⊢ (? % ?).
1849      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1850       [apply le_A_exp
1851       |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1852         [apply le_times_r.
1853          apply H
1854           [rewrite > H3.
1855            rewrite > times_n_SO in ⊢ (? % ?).
1856            rewrite > sym_times.
1857            apply lt_times_l1
1858             [apply lt_to_le.assumption
1859             |apply le_n
1860             ]
1861           |assumption
1862           ]
1863         |rewrite < H3.
1864          rewrite < assoc_times.
1865          rewrite > sym_times in ⊢ (? (? % ?) ?).
1866          rewrite > assoc_times.
1867          apply le_times
1868           [rewrite > H3.
1869            elim a[apply le_n|simplify.apply le_plus_n_r]
1870           |rewrite < exp_plus_times.
1871            apply le_exp
1872             [apply lt_O_S
1873             |apply (trans_le ? (m+(m-3)))
1874               [apply le_plus_l.
1875                cases m[apply le_n|apply le_n_Sn]
1876               |simplify.rewrite < plus_n_O.
1877                rewrite > eq_minus_plus_plus_minus
1878                 [apply le_n
1879                 |rewrite > H3.
1880                  apply (trans_le ? (2*2))
1881                   [simplify.apply (le_n_Sn 3)
1882                   |apply le_times_r.assumption
1883                   ]
1884                 ]
1885               ]
1886             ]
1887           ]
1888         ]
1889       ]
1890     |rewrite > H3.rewrite < H4.simplify.
1891      apply le_S_S.apply lt_O_S
1892     |apply not_lt_to_le.intro.
1893      apply (lt_to_not_le ? ? H1).
1894      rewrite > H3.
1895      apply (le_n_O_elim a)
1896       [apply le_S_S_to_le.assumption
1897       |apply le_O_n
1898       ]
1899     ]
1900   |elim (le_to_or_lt_eq O a (le_O_n ?))
1901     [apply (trans_le ? (A ((S(S O))*(S a))))
1902       [apply monotonic_A.
1903        rewrite > H3.
1904        rewrite > times_SSO.
1905        apply le_n_Sn
1906       |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1907         [apply le_A_exp
1908         |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1909           [apply le_times_r.
1910            apply H
1911             [rewrite > H3.
1912              apply le_S_S.
1913              apply le_S_times_SSO.
1914              assumption
1915             |apply le_S_S.assumption
1916             ]
1917           |rewrite > H3.
1918            change in ⊢ (? ? (? % ?)) with (2*a).
1919            rewrite > times_SSO.
1920            change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1921            rewrite > minus_Sn_m
1922             [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1923              rewrite < assoc_times in ⊢ (? (? ? %) ?).
1924              rewrite < assoc_times.
1925              rewrite > sym_times in ⊢ (? (? % ?) ?).
1926              rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1927              rewrite > assoc_times.
1928              apply le_times_r.
1929              rewrite < exp_plus_times.
1930              apply le_exp
1931               [apply lt_O_S
1932               |rewrite < eq_minus_plus_plus_minus
1933                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1934                  apply le_n
1935                 |apply le_S_S.
1936                  apply O_lt_const_to_le_times_const.
1937                  assumption
1938                 ]
1939               ]
1940             |apply le_S_S.
1941              apply O_lt_const_to_le_times_const.
1942              assumption
1943             ]
1944           ]
1945         ]
1946       ]
1947     |rewrite < H4 in H3.simplify in H3.
1948      apply False_ind.
1949      apply (lt_to_not_le ? ? H1).
1950      rewrite > H3.
1951      apply le_n
1952     ]
1953   ]
1954 qed.
1955
1956 theorem le_n_SSSSSSSSO_to_le_A_exp: 
1957 \forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
1958 intro.cases n
1959   [intro.apply le_n
1960   |cases n1
1961     [intro.apply le_n
1962     |cases n2
1963       [intro.apply le_n
1964       |cases n3
1965         [intro.apply leb_true_to_le.reflexivity
1966         |cases n4
1967           [intro.apply leb_true_to_le.reflexivity
1968           |cases n5
1969             [intro.apply leb_true_to_le.reflexivity
1970             |cases n6
1971               [intro.apply leb_true_to_le.reflexivity
1972               |cases n7
1973                 [intro.apply leb_true_to_le.reflexivity
1974                 |cases n8
1975                   [intro.apply leb_true_to_le.reflexivity
1976                   |intro.apply False_ind.
1977                    apply (lt_to_not_le ? ? H).
1978                    apply leb_true_to_le.reflexivity
1979                   ]
1980                 ]
1981               ]
1982             ]
1983           ]
1984         ]
1985       ]
1986     ]
1987   ]
1988 qed.
1989            
1990 theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
1991 intro.
1992 apply (nat_elim1 n).
1993 intros.
1994 elim (decidable_le 9 m)
1995   [elim (or_eq_eq_S m).
1996    elim H2
1997     [rewrite > H3 in ⊢ (? % ?).
1998      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1999       [apply le_A_exp
2000       |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
2001         [apply le_times_r.
2002          apply H.
2003          rewrite > H3. 
2004          apply lt_m_nm
2005           [apply (trans_lt ? 4)
2006             [apply lt_O_S
2007             |apply (lt_times_to_lt 2)
2008               [apply lt_O_S
2009               |rewrite < H3.assumption
2010               ]
2011             ]
2012           |apply le_n
2013           ]
2014         |rewrite < H3.
2015          rewrite < exp_plus_times.
2016          apply le_exp
2017           [apply lt_O_S
2018           |simplify.rewrite < plus_n_O.
2019            rewrite > eq_minus_plus_plus_minus
2020             [apply le_plus_l.
2021              apply le_pred_n
2022             |apply (trans_le ? 9)
2023               [apply leb_true_to_le. reflexivity
2024               |assumption
2025               ]
2026             ]
2027           ]
2028         ]
2029       ]
2030     |apply (trans_le ? (A (2*(S a))))
2031       [apply monotonic_A.
2032        rewrite > H3.
2033        rewrite > times_SSO.
2034        apply le_n_Sn
2035       |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
2036         [apply lt_SSSSO_to_le_A_exp.
2037          apply le_S_S.
2038          apply (le_times_to_le 2)
2039           [apply le_n_Sn.
2040           |apply le_S_S_to_le.rewrite < H3.assumption
2041           ]
2042         |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
2043           [apply le_times_r.
2044            apply H.
2045            rewrite > H3.
2046            apply le_S_S. 
2047            apply lt_m_nm
2048             [apply (lt_to_le_to_lt ? 4)
2049               [apply lt_O_S
2050               |apply (le_times_to_le 2)
2051                 [apply lt_O_S
2052                 |apply le_S_S_to_le.
2053                  rewrite < H3.assumption
2054                 ]
2055               ]
2056             |apply le_n
2057             ]
2058           |rewrite > times_SSO.
2059            rewrite < H3.
2060            rewrite < exp_plus_times.
2061            apply le_exp
2062             [apply lt_O_S
2063             |cases m
2064               [apply le_n
2065               |cases n1
2066                 [apply le_n
2067                 |simplify.
2068                  rewrite < minus_n_O.
2069                  rewrite < plus_n_O.
2070                  rewrite < plus_n_Sm.
2071                  simplify.rewrite < minus_n_O.
2072                  rewrite < plus_n_Sm.
2073                  apply le_n
2074                 ]
2075               ]
2076             ]
2077           ]
2078         ]
2079       ]
2080     ]
2081   |apply le_n_SSSSSSSSO_to_le_A_exp.
2082    apply le_S_S_to_le.
2083    apply not_le_to_lt.
2084    assumption
2085   ]
2086 qed.       
2087
2088 theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n).
2089 intros.
2090 apply (trans_le ? ((exp 2 (2*n))/(2*n)))
2091   [apply le_times_to_le_div
2092     [rewrite > (times_n_O O) in ⊢ (? % ?).
2093      apply lt_times
2094       [apply lt_O_S
2095       |assumption
2096       ]
2097     |simplify in ⊢ (? ? (? ? %)).
2098      rewrite < plus_n_O.
2099      rewrite > exp_plus_times.
2100      apply le_times_l.
2101      alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con".
2102      apply le_times_SSO_n_exp_SSO_n
2103     ]
2104   |apply le_times_to_le_div2
2105     [rewrite > (times_n_O O) in ⊢ (? % ?).
2106      apply lt_times
2107       [apply lt_O_S
2108       |assumption
2109       ]
2110     |apply (trans_le ? ((B (2*n)*(2*n))))
2111       [rewrite < sym_times in ⊢ (? ? %).
2112        apply le_exp_B.
2113        assumption
2114       |apply le_times_l.
2115        apply le_B_A
2116       ]
2117     ]
2118   ]
2119 qed.
2120
2121 theorem le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n.
2122 intros.
2123 apply (trans_le ? (A(n/2*2)))
2124   [rewrite > sym_times.
2125    apply le_exp_Al.
2126    elim (le_to_or_lt_eq ? ? (le_O_n (n/2)))
2127     [assumption
2128     |apply False_ind.
2129      apply (lt_to_not_le ? ? H).
2130      rewrite > (div_mod n 2)
2131       [rewrite < H1.
2132        change in ⊢ (? % ?) with (n\mod 2).
2133        apply le_S_S_to_le.
2134        apply lt_mod_m_m.
2135        apply lt_O_S
2136       |apply lt_O_S
2137       ]
2138     ]
2139   |apply monotonic_A.
2140    rewrite > (div_mod n 2) in ⊢ (? ? %).
2141    apply le_plus_n_r.
2142    apply lt_O_S
2143   ]
2144 qed.
2145
2146 theorem eq_sigma_pi_SO_n: \forall n.
2147 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
2148 intro.elim n
2149   [reflexivity
2150   |rewrite > true_to_sigma_p_Sn
2151     [rewrite > H.reflexivity
2152     |reflexivity
2153     ]
2154   ]
2155 qed.
2156
2157 theorem leA_prim: \forall n.
2158 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
2159 intro.
2160 unfold prim.
2161 rewrite < (exp_sigma_p (S n) n primeb).
2162 unfold A.
2163 rewrite < times_pi_p.
2164 apply le_pi_p.
2165 intros.
2166 rewrite > sym_times.
2167 change in ⊢ (? ? %) with (exp i (S (log i n))).
2168 apply lt_to_le.
2169 apply lt_exp_log.
2170 apply prime_to_lt_SO.
2171 apply primeb_true_to_prime.
2172 assumption.
2173 qed.
2174
2175
2176 theorem le_prim_log : \forall n,b.S O < b \to
2177 log b (A n) \leq prim n * (S (log b n)).
2178 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
2179   [apply le_log
2180      [assumption
2181      |apply le_Al]
2182   |assumption]
2183 qed.
2184
2185
2186 (* the inequalities *)
2187 theorem le_exp_priml: \forall n. O < n \to
2188 exp 2 (2*n) \le exp (2*n) (S(prim (2*n))).
2189 intros.
2190 apply (trans_le ? (((2*n*(B (2*n))))))
2191   [apply le_exp_B.assumption
2192   |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))).
2193    apply le_times_r.
2194    apply (trans_le ? (A (2*n)))
2195     [apply le_B_A
2196     |apply le_Al
2197     ]
2198   ]
2199 qed.
2200
2201 theorem le_exp_prim4l: \forall n. O < n \to
2202 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
2203 intros.
2204 apply (trans_le ? (2*(4*n*(B (4*n)))))
2205   [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
2206    apply le_times_r.
2207    cut (4*n = 2*(2*n))
2208     [rewrite > Hcut.
2209      apply le_exp_B.
2210      apply lt_to_le.unfold.
2211      rewrite > times_n_SO in ⊢ (? % ?).
2212      apply le_times_r.assumption
2213     |rewrite < assoc_times.
2214      reflexivity
2215     ]
2216   |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
2217    rewrite < assoc_times.
2218    rewrite > sym_times in ⊢ (? (? % ?) ?).
2219    rewrite > assoc_times.
2220    apply le_times_r.
2221    apply (trans_le ? (A (4*n)))
2222     [apply le_B_A4.assumption
2223     |apply le_Al
2224     ]
2225   ]
2226 qed.
2227
2228 theorem le_priml: \forall n. O < n \to
2229 2*n \le (S (log 2 (2*n)))*S(prim (2*n)).
2230 intros.
2231 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
2232   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
2233     [apply le_log
2234       [apply le_n
2235       |apply le_exp_priml.assumption
2236       ]
2237     |rewrite > sym_times in ⊢ (? ? %). 
2238      apply log_exp1.
2239      apply le_n
2240     ]
2241   |apply le_n
2242   ]
2243 qed.
2244
2245 theorem le_exp_primr: \forall n.
2246 exp n (prim n) \le exp 2 (2*(2*n-3)).
2247 intros.
2248 apply (trans_le ? (exp (A n) 2))
2249   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
2250    rewrite < times_n_SO.
2251    apply leA_r2
2252   |rewrite > sym_times.
2253    rewrite < exp_exp_times.
2254    apply monotonic_exp1.
2255    apply le_A_exp5
2256   ]
2257 qed.
2258
2259 (* bounds *)
2260 theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n.
2261 intros.
2262 apply le_times_to_le_div
2263   [apply lt_O_log
2264     [apply lt_to_le.assumption
2265     |assumption
2266     ]
2267   |apply (trans_le ? (log 2 (exp n (prim n))))
2268     [rewrite > sym_times.
2269      apply log_exp2
2270       [apply le_n
2271       |apply lt_to_le.assumption
2272       ]
2273     |rewrite < (eq_log_exp 2) in ⊢ (? ? %)
2274       [apply le_log
2275         [apply le_n
2276         |apply le_exp_primr
2277         ]
2278       |apply le_n
2279       ]
2280     ]
2281   ]
2282 qed.
2283      
2284 theorem le_priml1: \forall n. O < n \to
2285 2*n/((log 2 n)+2) - 1 \le prim (2*n).
2286 intros.
2287 apply le_plus_to_minus.
2288 apply le_times_to_le_div2
2289   [rewrite > sym_plus.
2290    simplify.apply lt_O_S
2291   |rewrite > sym_times in ⊢ (? ? %).
2292    rewrite < plus_n_Sm.
2293    rewrite < plus_n_Sm in ⊢ (? ? (? ? %)).
2294    rewrite < plus_n_O.
2295    rewrite < sym_plus.
2296    rewrite < log_exp
2297     [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)).
2298      apply le_priml.
2299      assumption
2300     |apply le_n
2301     |assumption
2302     ]
2303   ]
2304 qed.
2305
2306 (*
2307 theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n.
2308 intros.
2309 apply lt_to_lt_O_minus.
2310 change in ⊢ (? ? (? (? % ?))) with (2*4).
2311 rewrite > assoc_times.
2312 apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n))
2313   [apply le_primr.apply (trans_lt ? ? ? ? H).
2314    apply leb_true_to_le.reflexivity
2315   |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1))
2316     [elim H
2317       [
2318 normalize in ⊢ (%);simplify.
2319     |apply le_priml1.
2320 *)   
2321
2322
2323