1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/chebishev".
18 include "nat/pi_p.ma".
19 include "nat/factorization.ma".
20 include "nat/factorial2.ma".
22 definition prim: nat \to nat \def
23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
25 definition A: nat \to nat \def
26 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
28 theorem le_Al1: \forall n.
29 A n \le pi_p (S n) primeb (\lambda p.n).
40 theorem le_Al: \forall n.
41 A n \le exp n (prim n).
43 rewrite < exp_sigma_p.
47 theorem leA_r2: \forall n.
48 exp n (prim n) \le A n * A n.
50 elim (le_to_or_lt_eq ? ? (le_O_n n))
51 [rewrite < (exp_sigma_p (S n) n primeb).
56 rewrite < exp_plus_times.
57 apply (trans_le ? (exp i (S(log i n))))
61 apply primeb_true_to_prime.
65 apply primeb_true_to_prime.
78 |rewrite < H. apply le_n
82 definition A': nat \to nat \def
83 \lambda n. pi_p (S n) primeb
84 (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
86 theorem eq_A_A': \forall n.A n = A' n.
87 intro.unfold A.unfold A'.
91 apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
92 [apply eq_f.apply sym_eq.apply sigma_p_true
93 |apply sym_eq.apply exp_sigma_p
98 theorem eq_pi_p_primeb_divides_b: \forall n,m.
99 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
100 = pi_p n primeb (\lambda p.exp p (ord m p)).
104 |apply (bool_elim ? (primeb n1));intro
105 [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
106 [apply (bool_elim ? (divides_b n1 m));intro
107 [rewrite > true_to_pi_p_Sn
110 |apply true_to_true_to_andb_true;assumption
112 |rewrite > false_to_pi_p_Sn
113 [rewrite > not_divides_to_ord_O
114 [simplify in ⊢ (? ? ? (? % ?)).
116 rewrite < times_n_SO.
118 |apply primeb_true_to_prime.assumption
119 |apply divides_b_false_to_not_divides.
122 |rewrite > H1.rewrite > H2.reflexivity
127 |rewrite > false_to_pi_p_Sn
128 [rewrite > false_to_pi_p_Sn
132 |rewrite > H1.reflexivity
138 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
139 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
142 apply (not_le_Sn_O ? H1)
143 |apply (bool_elim ? (primeb n∧divides_b n m));intro
144 [rewrite > true_to_pi_p_Sn
145 [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
147 rewrite > (H (ord_rem m n))
150 apply (bool_elim ? (primeb x));intro
152 apply (bool_elim ? (divides_b x (ord_rem m n)));intro
154 apply divides_to_divides_b_true
155 [apply prime_to_lt_O.
156 apply primeb_true_to_prime.
158 |apply (trans_divides ? (ord_rem m n))
159 [apply divides_b_true_to_divides.
161 |apply divides_ord_rem
162 [apply (trans_lt ? x)
163 [apply prime_to_lt_SO.
164 apply primeb_true_to_prime.
173 apply not_divides_to_divides_b_false
174 [apply prime_to_lt_O.
175 apply primeb_true_to_prime.
177 |apply ord_O_to_not_divides
179 |apply primeb_true_to_prime.
181 |rewrite < (ord_ord_rem n)
182 [apply not_divides_to_ord_O
183 [apply primeb_true_to_prime.
185 |apply divides_b_false_to_not_divides.
189 |apply primeb_true_to_prime.
190 apply (andb_true_true ? ? H3)
191 |apply primeb_true_to_prime.
204 |apply primeb_true_to_prime.
205 apply (andb_true_true ? ? H3)
206 |apply primeb_true_to_prime.
207 apply (andb_true_true ? ? H5)
212 [apply prime_to_lt_SO.
213 apply primeb_true_to_prime.
214 apply (andb_true_true ? ? H3)
217 |apply not_eq_to_le_to_lt
218 [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
220 intro.rewrite > H7 in H6.simplify in H6.
221 apply (not_divides_ord_rem m n)
223 |apply prime_to_lt_SO.
224 apply primeb_true_to_prime.
225 apply (andb_true_true ? ? H3)
226 |apply divides_b_true_to_divides.
227 apply (andb_true_true_r ? ? H6)
229 |elim H4.rewrite > H6.
232 apply primeb_true_to_prime.
233 apply (andb_true_true ? ? H3)
235 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
239 |apply divides_ord_rem
240 [apply prime_to_lt_SO.
241 apply primeb_true_to_prime.
242 apply (andb_true_true ? ? H3)
246 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
247 [apply le_max_f_max_g.
249 apply (bool_elim ? (primeb i));intro
251 apply divides_to_divides_b_true
252 [apply prime_to_lt_O.
253 apply primeb_true_to_prime.
255 |apply (trans_divides ? (ord_rem m n))
256 [apply divides_b_true_to_divides.
257 apply (andb_true_true_r ? ? H5)
258 |apply divides_ord_rem
259 [apply prime_to_lt_SO.
260 apply primeb_true_to_prime.
261 apply (andb_true_true ? ? H3)
275 |apply prime_to_lt_SO.
276 apply primeb_true_to_prime.
277 apply (andb_true_true ? ? H3)
282 |elim (le_to_or_lt_eq ? ? H1)
283 [rewrite > false_to_pi_p_Sn
286 |apply false_to_lt_max
287 [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
289 apply lt_SO_max_prime.
302 rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
305 apply (bool_elim ? (primeb x));intro
307 change with (divides_b x (S O) =false).
308 apply not_divides_to_divides_b_false
309 [apply prime_to_lt_O.
310 apply primeb_true_to_prime.
313 apply (le_to_not_lt x (S O))
315 [apply lt_O_S.assumption
318 |elim (primeb_true_to_prime ? H6).
331 theorem pi_p_primeb_divides_b: \forall n. O < n \to
332 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
334 apply lt_max_to_pi_p_primeb
341 theorem pi_p_primeb: \forall n. O < n \to
342 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
344 rewrite < eq_pi_p_primeb_divides_b.
345 apply pi_p_primeb_divides_b.
349 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
352 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
356 |apply lt_O_ord_rem;assumption
363 theorem sigma_p_divides_b:
364 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
365 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
368 |simplify in ⊢ (? ? ? (? % ? ?)).
369 rewrite > true_to_sigma_p_Sn
370 [rewrite > sym_plus.rewrite < plus_n_SO.
372 rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
375 apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
377 apply divides_to_divides_b_true
381 |apply (witness ? ? ((exp p (n - x))*n1)).
382 rewrite < assoc_times.
383 rewrite < exp_plus_times.
385 [apply eq_f.simplify.
388 apply plus_minus_m_m.
389 apply lt_to_le.assumption
395 apply (divides_b_false_to_not_divides ? ? H5).
396 apply (witness ? ? ((exp p (n - S x))*n1)).
397 rewrite < assoc_times.
398 rewrite < exp_plus_times.
402 apply plus_minus_m_m.
409 |apply divides_to_divides_b_true
411 apply prime_to_lt_O.assumption
412 |apply (witness ? ? n1).reflexivity
418 theorem sigma_p_divides_b1:
419 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
420 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
422 lapply (prime_to_lt_SO ? H1) as H4.
423 lapply (prime_to_lt_O ? H1) as H5.
424 rewrite > (false_to_eq_sigma_p m k)
425 [apply sigma_p_divides_b;assumption
428 apply not_divides_to_divides_b_false
429 [apply lt_O_exp.assumption
430 |intro.apply (le_to_not_lt ? ? H6).
432 rewrite < (ord_exp p)
433 [rewrite > (plus_n_O m).
434 rewrite < (not_divides_to_ord_O ? ? H1 H2).
435 rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
437 [apply divides_to_le_ord
438 [apply lt_O_exp.assumption
439 |rewrite > (times_n_O O).
441 [apply lt_O_exp.assumption
447 |apply lt_O_exp.assumption
457 theorem eq_ord_sigma_p:
458 \forall n,m,x. O < n \to prime x \to
459 exp x m \le n \to n < exp x (S m) \to
460 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
462 lapply (prime_to_lt_SO ? H1).
463 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
464 [apply sigma_p_divides_b1
465 [apply lt_O_ord_rem;assumption
467 |apply not_divides_ord_rem;assumption
469 apply (le_to_lt_to_lt ? (log x n))
470 [apply le_ord_log;assumption
471 |apply (lt_exp_to_lt x)
473 |apply (le_to_lt_to_lt ? n ? ? H3).
484 theorem pi_p_primeb1: \forall n. O < n \to
485 n = pi_p (S n) primeb
486 (\lambda p.(pi_p (log p n)
487 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
489 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
493 rewrite > exp_sigma_p.
497 |apply primeb_true_to_prime.
499 |apply le_exp_log.assumption
501 apply prime_to_lt_SO.
502 apply primeb_true_to_prime.
508 theorem eq_fact_pi_p:\forall n. fact n =
509 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
512 |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
513 rewrite > true_to_pi_p_Sn
514 [apply eq_f.assumption
520 theorem eq_sigma_p_div: \forall n,q.O < q \to
521 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
524 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
525 [apply div_mod_spec_intro
526 [apply lt_mod_m_m.assumption
528 [simplify.elim q;reflexivity
529 |elim (or_div_mod1 n1 q)
531 rewrite > divides_to_mod_O
533 rewrite > true_to_sigma_p_Sn
534 [rewrite > H4 in ⊢ (? ? % ?).
539 apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
540 [apply div_mod_spec_div_mod.
542 |apply div_mod_spec_intro
543 [apply lt_mod_m_m.assumption
549 |apply true_to_true_to_andb_true
551 |apply divides_to_divides_b_true;assumption
558 rewrite > false_to_sigma_p_Sn
560 [rewrite < plus_n_Sm.
564 |elim (le_to_or_lt_eq (S (mod n1 q)) q)
568 apply (witness ? ? (S(div n1 q))).
569 rewrite < times_n_Sm.
571 rewrite < H2 in ⊢ (? ? ? (? ? %)).
578 |rewrite > not_divides_to_divides_b_false
579 [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
588 |apply div_mod_spec_div_mod.
593 theorem fact_pi_p: \forall n. fact n =
595 (\lambda p.(pi_p (log p n)
596 (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
598 rewrite > eq_fact_pi_p.
600 (pi_p (S n) (λi:nat.leb (S O) i)
601 (λn.pi_p (S n) primeb
602 (\lambda p.(pi_p (log p n)
603 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
604 [apply eq_pi_p1;intros
607 apply leb_true_to_le.assumption
610 (pi_p (S n) (λi:nat.leb (S O) i)
612 .pi_p (S n) (\lambda p.primeb p\land leb p n)
613 (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
616 |intros.apply eq_pi_p1
617 [intros.elim (primeb x1)
618 [simplify.apply sym_eq.
619 apply le_to_leb_true.
628 (pi_p (S n) (λi:nat.leb (S O) i)
630 .pi_p (S n) (λp:nat.primeb p∧leb p m)
631 (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
636 apply false_to_eq_pi_p
638 |intros.rewrite > lt_to_leb_false
639 [elim primeb;reflexivity|assumption]
642 |(* make a general theorem *)
646 .pi_p (S n) (λm.leb p m)
647 (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
651 apply (bool_elim ? (primeb y \land leb y x));intros
652 [rewrite > (le_to_leb_true (S O) x)
654 |apply (trans_le ? y)
655 [apply prime_to_lt_O.
656 apply primeb_true_to_prime.
657 apply (andb_true_true ? ? H2)
658 |apply leb_true_to_le.
659 apply (andb_true_true_r ? ? H2)
662 |elim (leb (S O) x);reflexivity
668 (pi_p (S n) (λm:nat.leb x m)
669 (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
674 apply false_to_eq_pi_p
676 [apply prime_to_lt_SO.
677 apply primeb_true_to_prime.
679 |apply (lt_to_le_to_lt ? x)
680 [apply prime_to_lt_O.
681 apply primeb_true_to_prime.
683 |apply leb_true_to_le.
690 apply not_divides_to_divides_b_false
693 apply primeb_true_to_prime.
696 apply (lt_to_not_le x1 (exp x (S i)))
697 [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
699 apply prime_to_lt_SO.
700 apply primeb_true_to_prime.
703 [apply prime_to_lt_O.
704 apply primeb_true_to_prime.
711 [apply (lt_to_le_to_lt ? x)
712 [apply prime_to_lt_O.
713 apply primeb_true_to_prime.
715 |apply leb_true_to_le.
726 (pi_p (log x n) (λi:nat.true)
727 (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
728 [apply (pi_p_pi_p1 (\lambda m,i.x)).
734 rewrite > exp_sigma_p.
737 (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
740 apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
741 [apply (bool_elim ? (leb x x2));intro
742 [rewrite > le_to_leb_true
744 |apply (trans_le ? x)
745 [apply prime_to_lt_O.
746 apply primeb_true_to_prime.
748 |apply leb_true_to_le.
752 |rewrite > lt_to_leb_false
754 |apply not_le_to_lt.intro.
755 apply (leb_false_to_not_le ? ? H6).
756 apply (trans_le ? (exp x (S x1)))
757 [rewrite > times_n_SO in ⊢ (? % ?).
758 change with (exp x (S O) \le exp x (S x1)).
760 [apply prime_to_lt_O.
761 apply primeb_true_to_prime.
763 |apply le_S_S.apply le_O_n.
767 |apply divides_b_true_to_divides.
774 rewrite < andb_sym in ⊢ (? ? ? %).
779 |apply eq_sigma_p_div.
782 apply primeb_true_to_prime.
795 (* odd n is just mod n (S(S O))
799 | S m \Rightarrow (S O) - odd m
802 theorem le_odd_SO: \forall n. odd n \le S O.
805 |simplify.cases (odd n1)
806 [simplify.apply le_n.
812 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
814 [apply (lt_O_n_elim ? H).
815 intro.simplify.reflexivity
819 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
820 pi_p (S ((S(S O))*n)) primeb
821 (\lambda p.(pi_p (log p ((S(S O))*n))
822 (\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)))))))).
823 intros.rewrite > fact_pi_p.
826 |intros.apply eq_pi_p
829 rewrite < exp_plus_times.
831 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
835 apply primeb_true_to_prime.
841 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
842 pi_p (S ((S(S O))*n)) primeb
843 (\lambda p.(pi_p (log p ((S(S O))*n))
844 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
845 pi_p (S ((S(S O))*n)) primeb
846 (\lambda p.(pi_p (log p ((S(S O))*n))
847 (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
849 rewrite < times_pi_p.
850 rewrite > fact_pi_p2.
857 theorem pi_p_primeb4: \forall n. S O < n \to
858 pi_p (S ((S(S O))*n)) primeb
859 (\lambda p.(pi_p (log p ((S(S O))*n))
860 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
863 (\lambda p.(pi_p (log p (S(S O)*n))
864 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
866 apply or_false_eq_SO_to_eq_pi_p
873 [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
874 rewrite < times_n_SO.
877 |simplify.rewrite < times_n_SO.assumption
881 |apply le_S_S_to_le.assumption
886 theorem pi_p_primeb5: \forall n. S O < n \to
887 pi_p (S ((S(S O))*n)) primeb
888 (\lambda p.(pi_p (log p ((S(S O))*n))
889 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
892 (\lambda p.(pi_p (log p n)
893 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
895 rewrite > (pi_p_primeb4 ? H).
896 apply eq_pi_p1;intros
898 |apply or_false_eq_SO_to_eq_pi_p
900 [apply prime_to_lt_SO.
901 apply primeb_true_to_prime.
903 |apply lt_to_le.assumption
909 [simplify.reflexivity
910 |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
912 apply prime_to_lt_SO.
913 apply primeb_true_to_prime.
916 [apply prime_to_lt_O.
917 apply primeb_true_to_prime.
928 theorem exp_fact_SSO: \forall n.
929 exp (fact n) (S(S O))
932 (\lambda p.(pi_p (log p n)
933 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
947 (\lambda p.(pi_p (log p n)
948 (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
950 theorem eq_fact_B:\forall n.S O < n \to
951 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
953 rewrite > fact_pi_p3.
956 rewrite > pi_p_primeb5
964 theorem le_B_A: \forall n. B n \le A n.
968 apply le_pi_p.intros.
969 apply le_pi_p.intros.
970 rewrite > exp_n_SO in ⊢ (? ? %).
972 [apply prime_to_lt_O.
973 apply primeb_true_to_prime.
981 theorem le_fact_A:\forall n.S O < n \to
982 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
991 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
992 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
994 apply (le_times_to_le (exp (fact n) (S(S O))))
998 [rewrite < sym_times in ⊢ (? ? %).
1000 rewrite < assoc_times.
1007 theorem le_B_exp: \forall n.
1008 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1012 [simplify.apply le_S.apply le_S.apply le_n
1013 |apply lt_SO_to_le_B_exp.
1014 apply le_S_S.apply lt_O_S.
1019 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1020 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1022 apply (le_times_to_le (exp (fact n) (S(S O))))
1025 |rewrite < assoc_times in ⊢ (? ? %).
1026 rewrite > sym_times in ⊢ (? ? (? % ?)).
1027 rewrite > assoc_times in ⊢ (? ? %).
1029 [rewrite < sym_times.
1031 apply lt_to_le.assumption
1037 theorem le_exp_B: \forall n. O < n \to
1038 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1042 |apply lt_SO_to_le_exp_B.
1043 apply le_S_S.assumption
1047 theorem eq_A_SSO_n: \forall n.O < n \to
1049 pi_p (S ((S(S O))*n)) primeb
1050 (\lambda p.(pi_p (log p ((S(S O))*n) )
1051 (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1054 rewrite > eq_A_A'.rewrite > eq_A_A'.
1057 pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1058 = pi_p (S ((S(S O))*n)) primeb
1059 (λ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))))))))
1061 rewrite < times_pi_p.
1062 apply eq_pi_p1;intros
1064 |rewrite < times_pi_p.
1065 apply eq_pi_p;intros
1067 |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1068 [simplify.rewrite < times_n_SO.apply times_n_SO
1069 |simplify.rewrite < plus_n_O.apply times_n_SO
1073 |apply (trans_eq ? ? (pi_p (S n) primeb
1074 (\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))))))))
1075 [apply eq_pi_p1;intros
1077 |apply eq_pi_p1;intros
1079 |rewrite > lt_to_leb_false
1080 [simplify.apply times_n_SO
1082 apply (trans_le ? (exp x (log x n)))
1084 [apply prime_to_lt_O.
1085 apply primeb_true_to_prime.
1095 |apply (trans_eq ? ?
1096 (pi_p (S ((S(S O))*n)) primeb
1097 (λp:nat.pi_p (log p n) (λi:nat.true)
1098 (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1100 apply or_false_eq_SO_to_eq_pi_p
1105 rewrite > lt_to_log_O
1111 |apply eq_pi_p1;intros
1114 apply or_false_eq_SO_to_eq_pi_p
1116 [apply prime_to_lt_SO.
1117 apply primeb_true_to_prime.
1124 rewrite > le_to_leb_true
1125 [simplify.reflexivity
1126 |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1128 apply prime_to_lt_SO.
1129 apply primeb_true_to_prime.
1132 [apply prime_to_lt_O.
1133 apply primeb_true_to_prime.
1135 |apply le_S_S.assumption
1146 theorem le_A_BA1: \forall n. O < n \to
1147 A((S(S O))*n) \le B((S(S O))*n)*A n.
1149 rewrite > eq_A_SSO_n
1152 apply le_pi_p.intros.
1153 apply le_pi_p.intros.
1155 [apply prime_to_lt_O.
1156 apply primeb_true_to_prime.
1158 |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1159 [simplify in ⊢ (? % ?).
1160 cut ((S(S O))*n/i\sup(S i1) = S O)
1161 [rewrite > Hcut.apply le_n
1162 |apply (div_mod_spec_to_eq
1163 ((S(S O))*n) (exp i (S i1))
1164 ? (mod ((S(S O))*n) (exp i (S i1)))
1165 ? (minus ((S(S O))*n) (exp i (S i1))) )
1166 [apply div_mod_spec_div_mod.
1168 apply prime_to_lt_O.
1169 apply primeb_true_to_prime.
1171 |cut (i\sup(S i1)≤(S(S O))*n)
1172 [apply div_mod_spec_intro
1173 [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
1174 apply lt_plus_to_lt_minus
1176 |simplify in ⊢ (? % ?).
1179 [apply leb_true_to_le.assumption
1180 |apply leb_true_to_le.assumption
1183 |rewrite > sym_plus.
1184 rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1185 rewrite < times_n_SO.
1186 apply plus_minus_m_m.
1189 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1191 [apply prime_to_lt_O.
1192 apply primeb_true_to_prime.
1197 rewrite > (times_n_O O) in ⊢ (? % ?).
1213 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1216 |apply le_A_BA1.apply lt_O_S
1220 theorem le_A_exp: \forall n.
1221 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1223 apply (trans_le ? (B((S(S O))*n)*A n))
1230 theorem le_A_exp1: \forall n.
1231 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1233 [simplify.apply le_S_S.apply le_O_n
1234 |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1235 apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1237 |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
1240 |rewrite < exp_plus_times.
1241 simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1248 theorem monotonic_A: monotonic nat le A.
1252 |apply (trans_le ? (A n1))
1255 cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1256 ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1257 [apply (bool_elim ? (primeb (S n1)));intro
1258 [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1259 rewrite > times_n_SO in ⊢ (? % ?).
1260 rewrite > sym_times.
1262 [apply lt_O_exp.apply lt_O_S
1265 |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1268 |apply le_pi_p.intros.
1270 [apply prime_to_lt_O.
1271 apply primeb_true_to_prime.
1274 [apply prime_to_lt_SO.
1275 apply primeb_true_to_prime.
1277 |apply (lt_to_le_to_lt ? i)
1278 [apply prime_to_lt_O.
1279 apply primeb_true_to_prime.
1281 |apply le_S_S_to_le.
1284 |apply le_S.apply le_n
1292 theorem le_A_exp2: \forall n. O < n \to
1293 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1295 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1300 |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1304 |rewrite > assoc_times.apply le_times_r.
1305 change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1315 theorem A_SO: A (S O) = S O.
1319 theorem A_SSO: A (S(S O)) = S (S O).
1323 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1327 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1332 theorem or_eq_eq_S: \forall n.\exists m.
1333 n = (S(S O))*m \lor n = S ((S(S O))*m).
1335 [apply (ex_intro ? ? O).
1338 [apply (ex_intro ? ? a).
1339 right.apply eq_f.assumption
1340 |apply (ex_intro ? ? (S a)).
1348 (* a better result *)
1349 theorem le_A_exp3: \forall n. S O < n \to
1350 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1352 apply (nat_elim1 n).
1354 elim (or_eq_eq_S m).
1356 [elim (le_to_or_lt_eq (S O) a)
1357 [rewrite > H3 in ⊢ (? % ?).
1358 apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1360 |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1361 ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1365 rewrite > times_n_SO in ⊢ (? % ?).
1366 rewrite > sym_times.
1368 [apply lt_to_le.assumption
1373 |rewrite > sym_times.
1374 rewrite > assoc_times.
1375 rewrite < exp_plus_times.
1377 (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1378 [rewrite > assoc_times.
1380 rewrite < exp_plus_times.
1386 apply le_S.apply le_S.
1390 rewrite > times_exp.
1391 apply monotonic_exp1.
1393 rewrite > sym_times.
1397 rewrite < plus_n_Sm.
1404 |rewrite < H4 in H3.
1408 apply le_S_S.apply le_S_S.apply le_O_n
1409 |apply not_lt_to_le.intro.
1410 apply (lt_to_not_le ? ? H1).
1412 apply (le_n_O_elim a)
1413 [apply le_S_S_to_le.assumption
1417 |elim (le_to_or_lt_eq O a (le_O_n ?))
1418 [apply (trans_le ? (A ((S(S O))*(S a))))
1421 rewrite > times_SSO.
1423 |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1425 |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1426 (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1432 rewrite > plus_n_SO.
1436 |apply le_S_S.assumption
1438 |rewrite > sym_times.
1439 rewrite > assoc_times.
1440 rewrite < exp_plus_times.
1442 (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1443 [rewrite > assoc_times.
1445 rewrite < exp_plus_times.
1448 |rewrite > times_SSO.
1451 rewrite < plus_n_Sm.
1456 rewrite > times_exp.
1457 apply monotonic_exp1.
1459 rewrite > sym_times.
1465 |rewrite < H4 in H3.simplify in H3.
1467 apply (lt_to_not_le ? ? H1).
1474 theorem eq_sigma_pi_SO_n: \forall n.
1475 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1478 |rewrite > true_to_sigma_p_Sn
1479 [rewrite > H.reflexivity
1485 theorem leA_prim: \forall n.
1486 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1489 rewrite < (exp_sigma_p (S n) n primeb).
1491 rewrite < times_pi_p.
1494 rewrite > sym_times.
1495 change in ⊢ (? ? %) with (exp i (S (log i n))).
1498 apply prime_to_lt_SO.
1499 apply primeb_true_to_prime.
1504 (* the inequalities *)
1505 theorem le_exp_priml: \forall n. O < n \to
1506 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1508 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1509 [apply le_exp_B.assumption
1510 |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1512 apply (trans_le ? (A ((S(S O))*n)))
1519 theorem le_priml: \forall n. O < n \to
1520 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1522 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1523 [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1526 |apply lt_O_exp.apply lt_O_S
1527 |apply le_exp_priml.assumption
1529 |rewrite > sym_times in ⊢ (? ? %).
1537 theorem le_exp_primr: \forall n. S O < n \to
1538 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
1540 apply (trans_le ? (exp (A n) (S(S O))))
1541 [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1542 rewrite < times_n_SO.
1544 |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
1545 [apply monotonic_exp1.
1548 |rewrite < times_exp.
1549 rewrite > exp_exp_times.
1550 rewrite > exp_exp_times.
1551 rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1552 rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
1560 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
1567 theorem le_exp_log: \forall p,n. O < n \to
1571 apply leb_true_to_le.
1573 apply (f_max_true (\lambda x.leb (exp p x) n)).
1574 apply (ex_intro ? ? O).
1577 |apply le_to_leb_true.simplify.assumption
1581 theorem lt_log_n_n: \forall n. O < n \to log n < n.
1584 [elim (le_to_or_lt_eq ? ? Hcut)
1586 |absurd (exp (S(S O)) n \le n)
1587 [rewrite < H1 in ⊢ (? (? ? %) ?).
1590 |apply lt_to_not_le.
1595 |unfold log.apply le_max_n
1599 theorem le_log_n_n: \forall n. log n \le n.
1609 theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
1611 [simplify.apply le_S.apply le_n
1612 |apply not_le_to_lt.
1613 apply leb_false_to_not_le.
1614 apply (lt_max_to_false ? (S n1) (S (log (S n1))))
1615 [apply le_S_S.apply le_n
1616 |apply lt_log_n_n.apply lt_O_S
1621 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
1622 (\forall m. p < m \to f m = false)
1625 apply not_lt_to_le.intro.
1626 apply not_eq_true_false.
1627 rewrite < (H1 ? H2).
1633 theorem log_times1: \forall n,m. O < n \to O < m \to
1634 log (n*m) \le S(log n+log m).
1636 unfold in ⊢ (? (% ?) ?).
1637 apply f_false_to_le_max
1638 [apply (ex_intro ? ? O).
1641 |apply le_to_leb_true.
1643 rewrite > times_n_SO.
1644 apply le_times;assumption
1647 apply lt_to_leb_false.
1648 apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
1649 [apply lt_times;apply lt_exp_log
1650 |rewrite < exp_plus_times.
1654 rewrite < plus_n_Sm.
1661 theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
1666 [rewrite < times_n_O.
1668 |apply log_times1;apply lt_O_S
1673 theorem log_exp: \forall n,m.O < m \to
1674 log ((exp (S(S O)) n)*m)=n+log m.
1676 unfold log in ⊢ (? ? (% ?) ?).
1677 apply max_spec_to_max.
1687 rewrite > times_plus_l.
1688 apply (trans_le ? (S((S(S O))\sup(n1)*m)))
1689 [apply le_S_S.assumption
1690 |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
1691 [rewrite > (times_n_O O) in ⊢ (? % ?).
1697 |intro.simplify.apply le_S_S.
1703 apply le_to_leb_true.
1704 rewrite > exp_plus_times.
1711 apply lt_to_leb_false.
1712 apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
1714 [apply lt_O_exp.apply lt_O_S
1717 |rewrite < exp_plus_times.
1720 |rewrite < plus_n_Sm.
1727 theorem log_SSO: \forall n. O < n \to
1728 log ((S(S O))*n) = S (log n).
1730 change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
1731 rewrite > log_exp.reflexivity.assumption.
1734 theorem or_eq_S: \forall n.\exists m.
1735 (n = (S(S O))*m) \lor (n = S((S(S O))*m)).
1738 [apply (ex_intro ? ? O).left.apply times_n_O
1740 [apply (ex_intro ? ? a).right.apply eq_f.assumption
1741 |apply (ex_intro ? ? (S a)).left.
1742 rewrite > H2.simplify.
1744 rewrite < plus_n_Sm.
1750 theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
1751 ((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
1755 [apply (ex_intro ? ? a).split
1757 rewrite > times_n_SO in ⊢ (? % ?).
1758 rewrite > sym_times.
1760 [apply (divides_to_lt_O a n ? ?)
1762 |apply (witness a n (S (S O))).
1763 rewrite > sym_times.
1770 |apply (ex_intro ? ? a).split
1772 apply (le_to_lt_to_lt ? ((S(S O))*a))
1773 [rewrite > times_n_SO in ⊢ (? % ?).
1774 rewrite > sym_times.
1784 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
1785 intro.simplify.reflexivity.
1788 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
1792 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
1793 intro.simplify.rewrite < plus_n_Sm.reflexivity.
1796 theorem fact1: \forall n.
1797 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
1799 [rewrite < times_n_O.apply le_n
1800 |rewrite > times_SSO.
1803 rewrite < assoc_times.
1805 apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
1807 rewrite > times_SSO.
1810 |rewrite > assoc_times.
1811 rewrite > assoc_times.
1812 rewrite > assoc_times in ⊢ (? ? %).
1814 rewrite > assoc_times in ⊢ (? ? %).
1816 rewrite < assoc_times.
1817 rewrite < assoc_times.
1818 rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
1819 rewrite > assoc_times.
1820 rewrite > assoc_times.
1822 rewrite > assoc_times in ⊢ (? ? %).
1824 rewrite > sym_times in ⊢ (? ? %).
1825 rewrite > assoc_times in ⊢ (? ? %).
1826 rewrite > assoc_times in ⊢ (? ? %).
1828 rewrite < assoc_times in ⊢ (? ? %).
1829 rewrite < assoc_times in ⊢ (? ? %).
1830 rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
1831 rewrite > assoc_times in ⊢ (? ? %).
1832 rewrite > assoc_times in ⊢ (? ? %).
1834 rewrite > sym_times in ⊢ (? ? (? ? %)).
1835 rewrite > sym_times in ⊢ (? ? %).
1841 theorem monotonic_log: monotonic nat le log.
1842 unfold monotonic.intros.
1843 elim (le_to_or_lt_eq ? ? H) 0
1847 apply (lt_exp_to_lt (S(S O)))
1849 |apply (le_to_lt_to_lt ? (S n))
1852 |apply (trans_lt ? y)
1859 |intro.rewrite < H1.apply le_n
1863 theorem lt_O_fact: \forall n. O < fact n.
1865 [simplify.apply lt_O_S
1867 rewrite > (times_n_O O).
1875 theorem fact2: \forall n.O < n \to
1876 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
1878 [simplify.apply le_S.apply le_n
1879 |rewrite > times_SSO.
1882 rewrite < assoc_times.
1884 rewrite < times_SSO in ⊢ (? ? %).
1885 apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
1886 [rewrite > assoc_times in ⊢ (? ? %).
1888 rewrite > assoc_times.
1889 rewrite > assoc_times.
1890 rewrite > assoc_times.
1893 rewrite > assoc_times.
1894 rewrite > sym_times in ⊢ (? ? %).
1895 rewrite > assoc_times in ⊢ (? ? %).
1896 rewrite > assoc_times in ⊢ (? ? %).
1898 rewrite > sym_times.
1899 rewrite > assoc_times.
1900 rewrite > assoc_times.
1902 rewrite < assoc_times.
1903 rewrite < assoc_times.
1904 rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1905 rewrite > assoc_times.
1906 rewrite > assoc_times.
1907 rewrite > sym_times in ⊢ (? ? %).
1909 rewrite < assoc_times.
1910 rewrite < sym_times.
1911 rewrite < assoc_times.
1914 [rewrite > (times_n_O O) in ⊢ (? % ?).
1916 [rewrite > (times_n_O O) in ⊢ (? % ?).
1929 theorem lt_O_log: \forall n. S O < n \to O < log n.
1931 [simplify.apply lt_O_S
1932 |apply (lt_to_le_to_lt ? (log n1))
1934 |apply monotonic_log.
1940 theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
1944 lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
1948 theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
1952 theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
1956 theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
1957 n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
1960 [rewrite > factS in ⊢ (? (? %) ?).
1961 rewrite > factS in ⊢ (? (? (? ? %)) ?).
1962 rewrite < assoc_times in ⊢ (? (? %) ?).
1963 rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
1964 rewrite > assoc_times in ⊢ (? (? %) ?).
1965 change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
1967 theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
1968 intro.apply (nat_elim1 n).
1970 elim (lt_O_to_or_eq_S m)
1974 apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1975 [apply monotonic_log.
1977 |rewrite > assoc_times in ⊢ (? (? %) ?).
1979 apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1982 |rewrite > plus_n_Sm.
1984 rewrite < times_n_Sm.
1985 apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
1989 |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
1994 |rewrite > times_SSO_n.
1995 rewrite > distr_times_minus.
1997 rewrite > plus_minus
1998 [rewrite > sym_plus.
1999 rewrite < assoc_times.
2001 |rewrite < assoc_times.
2002 rewrite > times_n_SO in ⊢ (? % ?).
2006 apply (lt_times_n_to_lt_r (S(S O)))
2008 |rewrite < times_n_SO.
2019 rewrite < eq_plus_minus_minus_plus.
2021 rewrite > assoc_plus.
2023 rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
2025 (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
2026 apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
2034 theorem stirling: \forall n,k.k \le n \to
2035 log (fact n) < n*log n - n + k*log n.
2037 apply (nat_elim1 n).
2039 elim (lt_O_to_or_eq_S m)
2043 apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
2044 [apply monotonic_log.
2046 |rewrite > assoc_times in ⊢ (? (? %) ?).
2048 apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
2051 |rewrite < plus_n_Sm.
2052 rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
2054 (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
2055 apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))