]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/chebyshev.ma
Dummy dependent products in inductive types arities are no longer cleaned.
[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.(S O)).
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 (* si dovrebbe poter migliorare *)
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 S O < 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.S O).
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) (λi:nat.leb (S O) i) 
801    (λn.pi_p (S n) primeb 
802     (\lambda p.(pi_p (log p n) 
803      (\lambda i.divides_b (exp p (S i)) n) (\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) (λi:nat.leb (S O) i)
811      (λn:nat
812       .pi_p (S n) (\lambda p.primeb p\land leb p n)
813        (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λ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) (λi:nat.leb (S O) i)
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 ((S(S O))*n) =
1013 pi_p (S ((S(S O))*n)) primeb 
1014   (\lambda p.(pi_p (log p ((S(S O))*n)) 
1015     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
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 ((S(S O))*n) =
1035 pi_p (S ((S(S O))*n)) primeb 
1036   (\lambda p.(pi_p (log p ((S(S O))*n)) 
1037     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
1038 pi_p (S ((S(S O))*n)) primeb 
1039   (\lambda p.(pi_p (log p ((S(S O))*n))   
1040     (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
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. S O < n \to
1051 pi_p (S ((S(S O))*n)) primeb 
1052   (\lambda p.(pi_p (log p ((S(S O))*n)) 
1053     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
1054
1055 pi_p (S n) primeb 
1056   (\lambda p.(pi_p (log p (S(S O)*n)) 
1057     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(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. S O < n \to
1080 pi_p (S ((S(S O))*n)) primeb 
1081   (\lambda p.(pi_p (log p ((S(S O))*n)) 
1082     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(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 ((S(S O))*(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) (S(S O))
1122
1123 pi_p (S n) primeb 
1124   (\lambda p.(pi_p (log p n) 
1125     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(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 ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*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 theorem le_fact_A:\forall n.S O < n \to
1280 fact (2*n) \le exp (fact n) 2 * A (2*n).
1281 intros.
1282 rewrite > eq_fact_B
1283   [apply le_times_r.
1284    apply le_B_A
1285   |assumption
1286   ]
1287 qed.
1288
1289 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1290 B (2*n) \le exp 2 (pred (2*n)).
1291 intros.
1292 apply (le_times_to_le (exp (fact n) (S(S O))))
1293   [apply lt_O_exp.
1294    apply lt_O_fact
1295   |rewrite < eq_fact_B
1296     [rewrite < sym_times in ⊢ (? ? %).
1297      rewrite > exp_SSO.
1298      rewrite < assoc_times.
1299      apply fact1
1300     |assumption
1301     ]
1302   ]
1303 qed.
1304
1305 theorem le_B_exp: \forall n.
1306 B (2*n) \le exp 2 (pred (2*n)).
1307 intro.cases n
1308   [apply le_n
1309   |cases n1
1310     [simplify.apply le_n
1311     |apply lt_SO_to_le_B_exp.
1312      apply le_S_S.apply lt_O_S.
1313     ]
1314   ]
1315 qed.
1316
1317 theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
1318 B (2*n) \le exp 2 ((2*n)-2).
1319 intros.
1320 apply (le_times_to_le (exp (fact n) (S(S O))))
1321   [apply lt_O_exp.
1322    apply lt_O_fact
1323   |rewrite < eq_fact_B
1324     [rewrite < sym_times in ⊢ (? ? %).
1325      rewrite > exp_SSO.
1326      rewrite < assoc_times.
1327      apply lt_SSSSO_to_fact.assumption
1328     |apply lt_to_le.apply lt_to_le.
1329      apply lt_to_le.assumption
1330     ]
1331   ]
1332 qed.
1333
1334 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1335 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1336 intros.
1337 apply (le_times_to_le (exp (fact n) (S(S O))))
1338   [apply lt_O_exp.
1339    apply lt_O_fact
1340   |rewrite < assoc_times in ⊢ (? ? %).
1341    rewrite > sym_times in ⊢ (? ? (? % ?)).
1342    rewrite > assoc_times in ⊢ (? ? %).
1343    rewrite < eq_fact_B
1344     [rewrite < sym_times.
1345      apply fact3.
1346      apply lt_to_le.assumption
1347     |assumption
1348     ]
1349   ]
1350 qed.
1351
1352 theorem le_exp_B: \forall n. O < n \to
1353 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1354 intros.
1355 elim H
1356   [apply le_n
1357   |apply lt_SO_to_le_exp_B.
1358    apply le_S_S.assumption
1359   ]
1360 qed.
1361
1362 theorem eq_A_SSO_n: \forall n.O < n \to
1363 A((S(S O))*n) =
1364  pi_p (S ((S(S O))*n)) primeb 
1365   (\lambda p.(pi_p (log p ((S(S O))*n) )   
1366     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1367  *A n.
1368 intro.
1369 rewrite > eq_A_A'.rewrite > eq_A_A'.
1370 unfold A'.intros.
1371 cut (
1372  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1373  = pi_p (S ((S(S O))*n)) primeb
1374     (λ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))))))))
1375   [rewrite > Hcut.
1376    rewrite < times_pi_p.
1377    apply eq_pi_p1;intros
1378     [reflexivity
1379     |rewrite < times_pi_p.
1380      apply eq_pi_p;intros
1381       [reflexivity
1382       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1383         [simplify.rewrite < times_n_SO.apply times_n_SO
1384         |simplify.rewrite < plus_n_O.apply times_n_SO
1385         ]
1386       ]
1387     ]
1388   |apply (trans_eq ? ? (pi_p (S n) primeb 
1389     (\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))))))))
1390     [apply eq_pi_p1;intros
1391       [reflexivity
1392       |apply eq_pi_p1;intros
1393         [reflexivity
1394         |rewrite > lt_to_leb_false
1395           [simplify.apply times_n_SO
1396           |apply le_S_S.
1397            apply (trans_le ? (exp x (log x n)))
1398             [apply le_exp
1399               [apply prime_to_lt_O.
1400                apply primeb_true_to_prime.
1401                assumption
1402               |assumption
1403               ]
1404             |apply le_exp_log.
1405              assumption
1406             ]
1407           ]
1408         ]
1409       ]
1410     |apply (trans_eq ? ? 
1411       (pi_p (S ((S(S O))*n)) primeb
1412        (λp:nat.pi_p (log p n) (λi:nat.true)
1413         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1414       [apply sym_eq.
1415        apply or_false_eq_SO_to_eq_pi_p
1416         [apply le_S_S.
1417          simplify.
1418          apply le_plus_n_r
1419         |intros.right.
1420          rewrite > lt_to_log_O
1421           [reflexivity
1422           |assumption
1423           |assumption
1424           ]
1425         ]
1426       |apply eq_pi_p1;intros
1427         [reflexivity
1428         |apply sym_eq.
1429          apply or_false_eq_SO_to_eq_pi_p
1430           [apply le_log
1431             [apply prime_to_lt_SO.
1432              apply primeb_true_to_prime.
1433              assumption
1434             |simplify.
1435              apply le_plus_n_r
1436             ]
1437           |intros.right.
1438            rewrite > le_to_leb_true
1439             [simplify.reflexivity
1440             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1441               [apply lt_exp_log.
1442                apply prime_to_lt_SO.
1443                apply primeb_true_to_prime.
1444                assumption
1445               |apply le_exp
1446                 [apply prime_to_lt_O.
1447                  apply primeb_true_to_prime.
1448                  assumption
1449                 |apply le_S_S.assumption
1450                 ]
1451               ]
1452             ]
1453           ]
1454         ]
1455       ]
1456     ]
1457   ]
1458 qed.
1459                
1460 theorem le_A_BA1: \forall n. O < n \to 
1461 A((S(S O))*n) \le B((S(S O))*n)*A n.
1462 intros.
1463 rewrite > eq_A_SSO_n
1464   [apply le_times_l.
1465    unfold B.
1466    apply le_pi_p.intros.
1467    apply le_pi_p.intros.
1468    apply le_exp
1469     [apply prime_to_lt_O.
1470      apply primeb_true_to_prime.
1471      assumption
1472     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1473       [simplify in ⊢ (? % ?).
1474        cut ((S(S O))*n/i\sup(S i1) = S O)
1475         [rewrite > Hcut.apply le_n
1476         |apply (div_mod_spec_to_eq 
1477           ((S(S O))*n) (exp i (S i1)) 
1478            ? (mod ((S(S O))*n) (exp i (S i1))) 
1479            ? (minus ((S(S O))*n) (exp i (S i1))) )
1480           [apply div_mod_spec_div_mod.
1481            apply lt_O_exp.
1482            apply prime_to_lt_O.
1483            apply primeb_true_to_prime.
1484            assumption
1485           |cut (i\sup(S i1)≤(S(S O))*n)
1486             [apply div_mod_spec_intro
1487               [apply lt_plus_to_lt_minus
1488                 [assumption
1489                 |simplify in ⊢ (? % ?).
1490                  rewrite < plus_n_O.
1491                  apply lt_plus
1492                   [apply leb_true_to_le.assumption
1493                   |apply leb_true_to_le.assumption
1494                   ]
1495                 ]
1496               |rewrite > sym_plus.
1497                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1498                rewrite < times_n_SO.
1499                apply plus_minus_m_m.
1500                assumption
1501               ]
1502             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1503               [apply le_exp
1504                 [apply prime_to_lt_O.
1505                  apply primeb_true_to_prime.
1506                  assumption
1507                 |assumption
1508                 ]
1509               |apply le_exp_log.
1510                rewrite > (times_n_O O) in ⊢ (? % ?).
1511                apply lt_times 
1512                 [apply lt_O_S
1513                 |assumption
1514                 ]
1515               ]
1516             ]
1517           ]
1518         ]
1519       |apply le_O_n
1520       ]
1521     ]
1522   |assumption
1523   ]
1524 qed.
1525
1526 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1527 intros.cases n
1528   [apply le_n
1529   |apply le_A_BA1.apply lt_O_S
1530   ]
1531 qed.
1532
1533 theorem le_A_exp: \forall n.
1534 A(2*n) \le (exp 2 (pred (2*n)))*A n.
1535 intro.
1536 apply (trans_le ? (B(2*n)*A n))
1537   [apply le_A_BA
1538   |apply le_times_l.
1539    apply le_B_exp
1540   ]
1541 qed.
1542
1543 theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
1544 A(2*n) \le exp 2 ((2*n)-2)*A n.
1545 intros.
1546 apply (trans_le ? (B(2*n)*A n))
1547   [apply le_A_BA
1548   |apply le_times_l.
1549    apply lt_SSSSO_to_le_B_exp.assumption
1550   ]
1551 qed.
1552
1553 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1554 intro.cases n
1555   [apply le_n
1556   |simplify.apply le_plus_r.
1557    apply le_n_Sn
1558   ]
1559 qed.
1560
1561 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1562 intros.
1563 elim H
1564   [apply le_n
1565   |rewrite > times_SSO.
1566    apply le_S_S.
1567    apply (trans_le ? (2*n1))
1568     [assumption
1569     |apply le_n_Sn
1570     ]
1571   ]
1572 qed.
1573
1574 theorem le_A_exp1: \forall n.
1575 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1576 intro.elim n
1577   [simplify.apply le_n
1578   |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1579    apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1580     [apply le_A_exp
1581     |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1582       [apply le_times_r.
1583        assumption
1584       |rewrite < exp_plus_times.
1585        apply le_exp
1586         [apply lt_O_S
1587         |cut (S(S n1) \le 2*(exp 2 n1))
1588           [apply le_S_S_to_le.
1589            change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1590            rewrite < S_pred
1591             [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1592              rewrite < S_pred
1593               [rewrite < eq_minus_plus_plus_minus
1594                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1595                  apply le_n
1596                 |assumption
1597                 ]
1598               |apply lt_to_lt_O_minus.
1599                apply (lt_to_le_to_lt ? (2*(S(S n1))))
1600                 [rewrite > times_n_SO in ⊢ (? % ?).
1601                  rewrite > sym_times.
1602                  apply lt_times_l1
1603                   [apply lt_O_S
1604                   |apply le_n
1605                   ]
1606                 |apply le_times_r.
1607                  assumption
1608                 ]
1609               ]
1610             |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1611              apply le_times
1612               [apply le_n_Sn
1613               |apply lt_O_exp.
1614                apply lt_O_S
1615               ]
1616             ]
1617           |elim n1
1618             [apply le_n
1619             |apply (trans_le ? (2*(S(S n2))))
1620               [apply le_S_times_SSO.
1621                apply lt_O_S
1622               |apply le_times_r.
1623                assumption
1624               ]
1625             ]
1626           ]
1627         ]
1628       ]
1629     ]
1630   ]
1631 qed.
1632
1633 theorem monotonic_A: monotonic nat le A.
1634 unfold.intros.
1635 elim H
1636   [apply le_n
1637   |apply (trans_le ? (A n1))
1638     [assumption
1639     |unfold A.
1640      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1641           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1642       [apply (bool_elim ? (primeb (S n1)));intro
1643         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1644          rewrite > times_n_SO in ⊢ (? % ?).
1645          rewrite > sym_times.
1646          apply le_times
1647           [apply lt_O_exp.apply lt_O_S
1648           |assumption
1649           ]
1650         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1651          assumption
1652         ]
1653       |apply le_pi_p.intros.
1654        apply le_exp
1655         [apply prime_to_lt_O.
1656          apply primeb_true_to_prime.
1657          assumption
1658         |apply le_log
1659           [apply prime_to_lt_SO.
1660            apply primeb_true_to_prime.
1661            assumption
1662           |apply le_S.apply le_n
1663           ]
1664         ]
1665       ]
1666     ]
1667   ]
1668 qed.
1669
1670 (*
1671 theorem le_A_exp2: \forall n. O < n \to
1672 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1673 intros.
1674 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1675   [apply monotonic_A.
1676    apply lt_to_le.
1677    apply lt_exp_log.
1678    apply le_n
1679   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1680     [apply le_A_exp1
1681     |apply le_exp
1682       [apply lt_O_S
1683       |rewrite > assoc_times.apply le_times_r.
1684        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1685        apply le_times_r.
1686        apply le_exp_log.
1687        assumption
1688       ]
1689     ]
1690   ]
1691 qed.
1692 *)
1693
1694 (* example *)
1695 theorem A_SO: A (S O) = S O.
1696 reflexivity.
1697 qed.
1698
1699 theorem A_SSO: A (S(S O)) = S (S O).
1700 reflexivity.
1701 qed.
1702
1703 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1704 reflexivity.
1705 qed.
1706
1707 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1708 reflexivity.
1709 qed.
1710
1711 (*
1712 (* a better result *)
1713 theorem le_A_exp3: \forall n. S O < n \to
1714 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1715 intro.
1716 apply (nat_elim1 n).
1717 intros.
1718 elim (or_eq_eq_S m).
1719 elim H2
1720   [elim (le_to_or_lt_eq (S O) a)
1721     [rewrite > H3 in ⊢ (? % ?).
1722      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1723       [apply le_A_exp
1724       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1725          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1726         [apply le_times_r.
1727          apply H
1728           [rewrite > H3.
1729            rewrite > times_n_SO in ⊢ (? % ?).
1730            rewrite > sym_times.
1731            apply lt_times_l1
1732             [apply lt_to_le.assumption
1733             |apply le_n
1734             ]
1735           |assumption
1736           ]
1737         |rewrite > sym_times.
1738          rewrite > assoc_times.
1739          rewrite < exp_plus_times.
1740          apply (trans_le ? 
1741           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1742           [rewrite > assoc_times.
1743            apply le_times_r.
1744            rewrite < exp_plus_times.
1745            apply le_exp
1746             [apply lt_O_S
1747             |rewrite < H3.
1748              simplify.
1749              rewrite < plus_n_O.
1750              apply le_S.apply le_S.
1751              apply le_n
1752             ]
1753           |apply le_times_l.
1754            rewrite > times_exp.
1755            apply monotonic_exp1.
1756            rewrite > H3.
1757            rewrite > sym_times.
1758            cases a
1759             [apply le_n
1760             |simplify.
1761              rewrite < plus_n_Sm.
1762              apply le_S.
1763              apply le_n
1764             ]
1765           ]
1766         ]
1767       ]
1768     |rewrite < H4 in H3.
1769      simplify in H3.
1770      rewrite > H3.
1771      simplify.
1772      apply le_S_S.apply le_S_S.apply le_O_n
1773     |apply not_lt_to_le.intro.
1774      apply (lt_to_not_le ? ? H1).
1775      rewrite > H3.
1776      apply (le_n_O_elim a)
1777       [apply le_S_S_to_le.assumption
1778       |apply le_O_n
1779       ]
1780     ]
1781   |elim (le_to_or_lt_eq O a (le_O_n ?))
1782     [apply (trans_le ? (A ((S(S O))*(S a))))
1783       [apply monotonic_A.
1784        rewrite > H3.
1785        rewrite > times_SSO.
1786        apply le_n_Sn
1787       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1788         [apply le_A_exp
1789         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1790            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1791           [apply le_times_r.
1792            apply H
1793             [rewrite > H3.
1794              apply le_S_S.
1795              simplify.
1796              rewrite > plus_n_SO.
1797              apply le_plus_r.
1798              rewrite < plus_n_O.
1799              assumption
1800             |apply le_S_S.assumption
1801             ]
1802           |rewrite > sym_times.
1803            rewrite > assoc_times.
1804            rewrite < exp_plus_times.
1805            apply (trans_le ? 
1806             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1807             [rewrite > assoc_times.
1808              apply le_times_r.
1809              rewrite < exp_plus_times.
1810              apply le_exp
1811               [apply lt_O_S
1812               |rewrite > times_SSO.
1813                rewrite < H3.
1814                simplify.
1815                rewrite < plus_n_Sm.
1816                rewrite < plus_n_O.
1817                apply le_n
1818               ]
1819             |apply le_times_l.
1820              rewrite > times_exp.
1821              apply monotonic_exp1.
1822              rewrite > H3.
1823              rewrite > sym_times.
1824              apply le_n
1825             ]
1826           ]
1827         ]
1828       ]
1829     |rewrite < H4 in H3.simplify in H3.
1830      apply False_ind.
1831      apply (lt_to_not_le ? ? H1).
1832      rewrite > H3.
1833      apply le_
1834     ]
1835   ]
1836 qed.
1837 *)
1838
1839 theorem le_A_exp4: \forall n. S O < n \to
1840 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1841 intro.
1842 apply (nat_elim1 n).
1843 intros.
1844 elim (or_eq_eq_S m).
1845 elim H2
1846   [elim (le_to_or_lt_eq (S O) a)
1847     [rewrite > H3 in ⊢ (? % ?).
1848      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1849       [apply le_A_exp
1850       |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1851         [apply le_times_r.
1852          apply H
1853           [rewrite > H3.
1854            rewrite > times_n_SO in ⊢ (? % ?).
1855            rewrite > sym_times.
1856            apply lt_times_l1
1857             [apply lt_to_le.assumption
1858             |apply le_n
1859             ]
1860           |assumption
1861           ]
1862         |rewrite < H3.
1863          rewrite < assoc_times.
1864          rewrite > sym_times in ⊢ (? (? % ?) ?).
1865          rewrite > assoc_times.
1866          apply le_times
1867           [rewrite > H3.
1868            elim a[apply le_n|simplify.apply le_plus_n_r]
1869           |rewrite < exp_plus_times.
1870            apply le_exp
1871             [apply lt_O_S
1872             |apply (trans_le ? (m+(m-3)))
1873               [apply le_plus_l.
1874                cases m[apply le_n|apply le_n_Sn]
1875               |simplify.rewrite < plus_n_O.
1876                rewrite > eq_minus_plus_plus_minus
1877                 [apply le_n
1878                 |rewrite > H3.
1879                  apply (trans_le ? (2*2))
1880                   [simplify.apply (le_n_Sn 3)
1881                   |apply le_times_r.assumption
1882                   ]
1883                 ]
1884               ]
1885             ]
1886           ]
1887         ]
1888       ]
1889     |rewrite > H3.rewrite < H4.simplify.
1890      apply le_S_S.apply lt_O_S
1891     |apply not_lt_to_le.intro.
1892      apply (lt_to_not_le ? ? H1).
1893      rewrite > H3.
1894      apply (le_n_O_elim a)
1895       [apply le_S_S_to_le.assumption
1896       |apply le_O_n
1897       ]
1898     ]
1899   |elim (le_to_or_lt_eq O a (le_O_n ?))
1900     [apply (trans_le ? (A ((S(S O))*(S a))))
1901       [apply monotonic_A.
1902        rewrite > H3.
1903        rewrite > times_SSO.
1904        apply le_n_Sn
1905       |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1906         [apply le_A_exp
1907         |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1908           [apply le_times_r.
1909            apply H
1910             [rewrite > H3.
1911              apply le_S_S.
1912              apply le_S_times_SSO.
1913              assumption
1914             |apply le_S_S.assumption
1915             ]
1916           |rewrite > H3.
1917            change in ⊢ (? ? (? % ?)) with (2*a).
1918            rewrite > times_SSO.
1919            change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1920            rewrite > minus_Sn_m
1921             [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1922              rewrite < assoc_times in ⊢ (? (? ? %) ?).
1923              rewrite < assoc_times.
1924              rewrite > sym_times in ⊢ (? (? % ?) ?).
1925              rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1926              rewrite > assoc_times.
1927              apply le_times_r.
1928              rewrite < exp_plus_times.
1929              apply le_exp
1930               [apply lt_O_S
1931               |rewrite < eq_minus_plus_plus_minus
1932                 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1933                  apply le_n
1934                 |apply le_S_S.
1935                  apply O_lt_const_to_le_times_const.
1936                  assumption
1937                 ]
1938               ]
1939             |apply le_S_S.
1940              apply O_lt_const_to_le_times_const.
1941              assumption
1942             ]
1943           ]
1944         ]
1945       ]
1946     |rewrite < H4 in H3.simplify in H3.
1947      apply False_ind.
1948      apply (lt_to_not_le ? ? H1).
1949      rewrite > H3.
1950      apply le_n
1951     ]
1952   ]
1953 qed.
1954
1955 theorem le_n_SSSSSSSSO_to_le_A_exp: 
1956 \forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
1957 intro.cases n
1958   [intro.apply le_n
1959   |cases n1
1960     [intro.apply le_n
1961     |cases n2
1962       [intro.apply le_n
1963       |cases n3
1964         [intro.apply leb_true_to_le.reflexivity
1965         |cases n4
1966           [intro.apply leb_true_to_le.reflexivity
1967           |cases n5
1968             [intro.apply leb_true_to_le.reflexivity
1969             |cases n6
1970               [intro.apply leb_true_to_le.reflexivity
1971               |cases n7
1972                 [intro.apply leb_true_to_le.reflexivity
1973                 |cases n8
1974                   [intro.apply leb_true_to_le.reflexivity
1975                   |intro.apply False_ind.
1976                    apply (lt_to_not_le ? ? H).
1977                    apply leb_true_to_le.reflexivity
1978                   ]
1979                 ]
1980               ]
1981             ]
1982           ]
1983         ]
1984       ]
1985     ]
1986   ]
1987 qed.
1988            
1989 theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
1990 intro.
1991 apply (nat_elim1 n).
1992 intros.
1993 elim (decidable_le 9 m)
1994   [elim (or_eq_eq_S m).
1995    elim H2
1996     [rewrite > H3 in ⊢ (? % ?).
1997      apply (trans_le ? (exp 2 (pred(2*a))*A a))
1998       [apply le_A_exp
1999       |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
2000         [apply le_times_r.
2001          apply H.
2002          rewrite > H3. 
2003          apply lt_m_nm
2004           [apply (trans_lt ? 4)
2005             [apply lt_O_S
2006             |apply (lt_times_to_lt 2)
2007               [apply lt_O_S
2008               |rewrite < H3.assumption
2009               ]
2010             ]
2011           |apply le_n
2012           ]
2013         |rewrite < H3.
2014          rewrite < exp_plus_times.
2015          apply le_exp
2016           [apply lt_O_S
2017           |simplify.rewrite < plus_n_O.
2018            rewrite > eq_minus_plus_plus_minus
2019             [apply le_plus_l.
2020              apply le_pred_n
2021             |apply (trans_le ? 9)
2022               [apply leb_true_to_le. reflexivity
2023               |assumption
2024               ]
2025             ]
2026           ]
2027         ]
2028       ]
2029     |apply (trans_le ? (A (2*(S a))))
2030       [apply monotonic_A.
2031        rewrite > H3.
2032        rewrite > times_SSO.
2033        apply le_n_Sn
2034       |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
2035         [apply lt_SSSSO_to_le_A_exp.
2036          apply le_S_S.
2037          apply (le_times_to_le 2)
2038           [apply le_n_Sn.
2039           |apply le_S_S_to_le.rewrite < H3.assumption
2040           ]
2041         |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
2042           [apply le_times_r.
2043            apply H.
2044            rewrite > H3.
2045            apply le_S_S. 
2046            apply lt_m_nm
2047             [apply (lt_to_le_to_lt ? 4)
2048               [apply lt_O_S
2049               |apply (le_times_to_le 2)
2050                 [apply lt_O_S
2051                 |apply le_S_S_to_le.
2052                  rewrite < H3.assumption
2053                 ]
2054               ]
2055             |apply le_n
2056             ]
2057           |rewrite > times_SSO.
2058            rewrite < H3.
2059            rewrite < exp_plus_times.
2060            apply le_exp
2061             [apply lt_O_S
2062             |cases m
2063               [apply le_n
2064               |cases n1
2065                 [apply le_n
2066                 |simplify.
2067                  rewrite < minus_n_O.
2068                  rewrite < plus_n_O.
2069                  rewrite < plus_n_Sm.
2070                  simplify.rewrite < minus_n_O.
2071                  rewrite < plus_n_Sm.
2072                  apply le_n
2073                 ]
2074               ]
2075             ]
2076           ]
2077         ]
2078       ]
2079     ]
2080   |apply le_n_SSSSSSSSO_to_le_A_exp.
2081    apply le_S_S_to_le.
2082    apply not_le_to_lt.
2083    assumption
2084   ]
2085 qed.       
2086
2087 theorem eq_sigma_pi_SO_n: \forall n.
2088 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
2089 intro.elim n
2090   [reflexivity
2091   |rewrite > true_to_sigma_p_Sn
2092     [rewrite > H.reflexivity
2093     |reflexivity
2094     ]
2095   ]
2096 qed.
2097
2098 theorem leA_prim: \forall n.
2099 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
2100 intro.
2101 unfold prim.
2102 rewrite < (exp_sigma_p (S n) n primeb).
2103 unfold A.
2104 rewrite < times_pi_p.
2105 apply le_pi_p.
2106 intros.
2107 rewrite > sym_times.
2108 change in ⊢ (? ? %) with (exp i (S (log i n))).
2109 apply lt_to_le.
2110 apply lt_exp_log.
2111 apply prime_to_lt_SO.
2112 apply primeb_true_to_prime.
2113 assumption.
2114 qed.
2115
2116
2117 theorem le_prim_log : \forall n,b.S O < b \to
2118 log b (A n) \leq prim n * (S (log b n)).
2119 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
2120   [apply le_log
2121      [assumption
2122      |apply le_Al]
2123   |assumption]
2124 qed.
2125
2126
2127 (* the inequalities *)
2128 theorem le_exp_priml: \forall n. O < n \to
2129 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
2130 intros.
2131 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
2132   [apply le_exp_B.assumption
2133   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
2134    apply le_times_r.
2135    apply (trans_le ? (A ((S(S O))*n)))
2136     [apply le_B_A
2137     |apply le_Al
2138     ]
2139   ]
2140 qed.
2141
2142 theorem le_exp_prim4l: \forall n. O < n \to
2143 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
2144 intros.
2145 apply (trans_le ? (2*(4*n*(B (4*n)))))
2146   [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
2147    apply le_times_r.
2148    cut (4*n = 2*(2*n))
2149     [rewrite > Hcut.
2150      apply le_exp_B.
2151      apply lt_to_le.unfold.
2152      rewrite > times_n_SO in ⊢ (? % ?).
2153      apply le_times_r.assumption
2154     |rewrite < assoc_times.
2155      reflexivity
2156     ]
2157   |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
2158    rewrite < assoc_times.
2159    rewrite > sym_times in ⊢ (? (? % ?) ?).
2160    rewrite > assoc_times.
2161    apply le_times_r.
2162    apply (trans_le ? (A (4*n)))
2163     [apply le_B_A4.assumption
2164     |apply le_Al
2165     ]
2166   ]
2167 qed.
2168
2169 theorem le_priml: \forall n. O < n \to
2170 2*n \le (S (log 2 (2*n)))*S(prim (2*n)).
2171 intros.
2172 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
2173   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
2174     [apply le_log
2175       [apply le_n
2176       |apply le_exp_priml.assumption
2177       ]
2178     |rewrite > sym_times in ⊢ (? ? %). 
2179      apply log_exp1.
2180      apply le_n
2181     ]
2182   |apply le_n
2183   ]
2184 qed.
2185
2186 theorem le_exp_primr: \forall n.
2187 exp n (prim n) \le exp 2 (2*(2*n-3)).
2188 intros.
2189 apply (trans_le ? (exp (A n) 2))
2190   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
2191    rewrite < times_n_SO.
2192    apply leA_r2
2193   |rewrite > sym_times.
2194    rewrite < exp_exp_times.
2195    apply monotonic_exp1.
2196    apply le_A_exp5
2197   ]
2198 qed.
2199
2200 (* bounds *)
2201 theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n.
2202 intros.
2203 apply le_times_to_le_div
2204   [apply lt_O_log
2205     [apply lt_to_le.assumption
2206     |assumption
2207     ]
2208   |apply (trans_le ? (log 2 (exp n (prim n))))
2209     [rewrite > sym_times.
2210      apply log_exp2
2211       [apply le_n
2212       |apply lt_to_le.assumption
2213       ]
2214     |rewrite < (eq_log_exp 2) in ⊢ (? ? %)
2215       [apply le_log
2216         [apply le_n
2217         |apply le_exp_primr
2218         ]
2219       |apply le_n
2220       ]
2221     ]
2222   ]
2223 qed.
2224      
2225 theorem le_priml1: \forall n. O < n \to
2226 2*n/((log 2 n)+2) - 1 \le prim (2*n).
2227 intros.
2228 apply le_plus_to_minus.
2229 apply le_times_to_le_div2
2230   [rewrite > sym_plus.
2231    simplify.apply lt_O_S
2232   |rewrite > sym_times in ⊢ (? ? %).
2233    rewrite < plus_n_Sm.
2234    rewrite < plus_n_Sm in ⊢ (? ? (? ? %)).
2235    rewrite < plus_n_O.
2236    rewrite < sym_plus.
2237    rewrite < log_exp
2238     [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)).
2239      apply le_priml.
2240      assumption
2241     |apply le_n
2242     |assumption
2243     ]
2244   ]
2245 qed.
2246
2247 (*
2248 theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n.
2249 intros.
2250 apply lt_to_lt_O_minus.
2251 change in ⊢ (? ? (? (? % ?))) with (2*4).
2252 rewrite > assoc_times.
2253 apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n))
2254   [apply le_primr.apply (trans_lt ? ? ? ? H).
2255    apply leb_true_to_le.reflexivity
2256   |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1))
2257     [elim H
2258       [
2259 normalize in ⊢ (%);simplify.
2260     |apply le_priml1.
2261 *)   
2262
2263
2264