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