+ |apply (le_exp_to_le1 ? ? (S (S O)));
+ [apply le_S;apply le_n
+ |do 2 rewrite > exp_SSO;apply (trans_le ? n)
+ [apply lt_to_le;assumption
+ |apply lt_to_le;apply leb_true_to_le;assumption]]]]]]]
+qed.
+
+lemma log_interval : \forall b,k,n. S O < b \to exp b k \leq n \to n < exp b (S k) \to
+ log b n = k.
+intros 2.elim k
+ [simplify in H2;rewrite < times_n_SO in H2;apply lt_to_log_O;assumption
+ |cut (log b n1 < S (S n))
+ [cut (n < log b n1)
+ [apply antisymmetric_le
+ [apply le_S_S_to_le;assumption
+ |assumption]
+ |apply (trans_le ? (log b (exp b (S n))))
+ [rewrite > eq_log_exp
+ [apply le_n
+ |assumption]
+ |apply le_log;assumption]]
+ |apply le_S_S;apply (trans_le ? (log b (pred (exp b (S (S n))))))
+ [apply le_log
+ [assumption
+ |apply le_S_S_to_le;apply (trans_le ? ? ? H3);
+ rewrite > minus_n_O in \vdash (? ? (? (? %)));
+ rewrite < (eq_minus_S_pred (exp b (S (S n))) O);
+ rewrite > minus_n_O in \vdash (? % ?);
+ apply minus_le_S_minus_S]
+ |unfold log;apply f_false_to_le_max;
+ [apply (ex_intro ? ? (S n));split
+ [apply (trans_le ? (exp b (S n)));
+ [apply lt_to_le;apply lt_m_exp_nm;assumption
+ |rewrite > minus_n_O in ⊢ (? ? (? %));
+ rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
+ rewrite > sym_plus;
+ change in \vdash (? % ?) with (S (O + exp b (S n)));
+ apply lt_minus_to_plus;
+ change in ⊢ (? ? (? % ?)) with (b * (exp b (S n)));
+ rewrite > times_n_SO in \vdash (? ? (? ? %));
+ rewrite > sym_times in \vdash (? ? (? % ?));
+ rewrite < distributive_times_minus;unfold lt;
+ rewrite > times_n_SO in \vdash (? % ?);apply le_times
+ [apply lt_O_exp;apply (trans_le ? ? ? ? H1);
+ apply le_S;apply le_n
+ |apply le_plus_to_minus_r;simplify;assumption]]
+ |apply le_to_leb_true;
+ rewrite > minus_n_O in \vdash (? ? (? %));
+ rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
+ rewrite > sym_plus;change in \vdash (? % ?) with (S (exp b (S n)));
+ apply lt_exp;
+ [assumption
+ |apply le_n]]
+ |intros;apply lt_to_leb_false;unfold lt;
+ rewrite > minus_n_O in \vdash (? (? (? %)) ?);
+ rewrite < eq_minus_S_pred;rewrite < minus_Sn_m
+ [rewrite > minus_S_S;rewrite < minus_n_O;apply le_exp;
+ [apply (trans_le ? ? ? ? H1);apply le_S;apply le_n
+ |assumption]
+ |apply lt_O_exp;apply (trans_le ? ? ? ? H1);apply le_S;apply le_n]]]]]
+qed.
+
+lemma log_strano : \forall b,i.S O < b \to S O < i \to
+ ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
+ (S (S (S O)))*i.
+alias num (instance 0) = "natural number".
+cut (\forall b,i,k.S O < b \to S O < i \to
+ (exp b k) \leq i-1 \to i-1 < (exp b (S k)) \to
+ ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
+ (S (S (S O)))*i)
+ [intros;apply (Hcut ? ? (log b (i-1)) H H1);
+ [apply le_exp_log;rewrite > (minus_n_n 1) in \vdash (? % ?);
+ apply lt_plus_to_lt_minus;
+ [apply le_n
+ |rewrite < eq_minus_plus_plus_minus
+ [rewrite > sym_plus;rewrite > eq_minus_plus_plus_minus;
+ [rewrite < minus_n_n;rewrite < plus_n_O;assumption
+ |apply le_n]
+ |apply lt_to_le;assumption]]
+ |apply lt_exp_log;assumption]
+ |intros;rewrite > minus_n_O in ⊢ (? (? (? ? (? ? (? %))) ?) ?);
+ rewrite < eq_minus_S_pred;rewrite > (log_interval ? k)
+ [apply (trans_le ? (3*(exp b k) + 3))
+ [change in \vdash (? (? ? %) ?) with (2+3);
+ rewrite < assoc_plus;apply le_plus_l;
+ elim k
+ [simplify;apply le_S;apply le_n
+ |elim (decidable_eq_nat O n)
+ [rewrite < H5;apply (trans_le ? (3*(exp 2 1)));
+ [simplify;apply le_n
+ |apply le_times_r;apply monotonic_exp1;assumption]
+ |rewrite < times_n_Sm;apply (trans_le ? (3*(exp b n) + 4))
+ [rewrite > assoc_plus;rewrite > sym_plus;apply le_plus_l;
+ assumption
+ |rewrite < sym_plus;change in \vdash (? % ?) with (S (3 + (3*(exp b n))));
+ apply lt_minus_to_plus;
+ change in ⊢ (? ? (? (? ? %) ?)) with (b*(exp b n));
+ rewrite > sym_times in \vdash (? ? (? (? ? %) ?));
+ rewrite < assoc_times;
+ rewrite > times_n_SO in ⊢ (? ? (? ? (? ? %)));
+ rewrite < assoc_times;rewrite < distr_times_minus;
+ apply (trans_le ? (3*2*1))
+ [simplify;apply le_S;apply le_S;apply le_n
+ |apply le_times
+ [apply le_times_r;apply (trans_le ? (exp 2 n))
+ [rewrite > exp_n_SO in \vdash (? % ?);apply le_exp
+ [apply le_S;apply le_n
+ |generalize in match H5;cases n
+ [intro;elim H6;reflexivity
+ |intro;apply le_S_S;apply le_O_n]]
+ |apply monotonic_exp1;assumption]
+ |apply le_S_S_to_le;rewrite < minus_Sn_m;
+ [simplify;rewrite < minus_n_O;assumption
+ |apply lt_to_le;assumption]]]]]]
+ |rewrite > times_n_SO in \vdash (? (? ? %) ?);
+ rewrite < distr_times_plus;apply le_times_r;
+ rewrite < plus_n_SO;apply (trans_le ? (S (i-1)))
+ [apply le_S_S;assumption
+ |rewrite < minus_Sn_m
+ [simplify;rewrite < minus_n_O;apply le_n
+ |apply lt_to_le;assumption]]]
+ |assumption
+ |assumption
+ |assumption]]
+qed.
+
+lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
+intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
+ [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
+ rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
+ rewrite > div_plus_times
+ [reflexivity
+ |generalize in match H;cases z;intros
+ [elim (not_le_Sn_O ? H2)
+ |apply lt_times_r;apply lt_mod_m_m;assumption]]
+ |assumption]
+qed.
+
+alias num (instance 0) = "natural number".
+lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
+ (sigma_p n (\lambda x.leb (S n) (x*x))
+ (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
+ ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
+ \leq ((28 * n * n!)/(pred (log b n))).
+intros.apply (trans_le ? (sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i. ((7*i)/(log b i))*(S (n!/i)))))
+ [apply le_sigma_p;intros;cut (b \leq i)
+ [cut (1 < i) [|apply (trans_le ? ? ? H Hcut)]
+ apply le_times_l;apply monotonic_div
+ [apply lt_O_log
+ [generalize in match H3;cases i
+ [simplify;intros;destruct H4
+ |intro;apply le_S_S;apply le_O_n]
+ |assumption]
+ |rewrite > sym_times;simplify in ⊢ (? (? (? % ?)) ?);
+ change in ⊢ (? % ?) with (1 + ((4 + (log b (pred i) * 4)) + 4*i));
+ rewrite > assoc_plus;rewrite < assoc_plus;
+ simplify in \vdash (? (? % ?) ?);rewrite < assoc_plus;
+ apply (trans_le ? (3*i + 4*i))
+ [apply le_minus_to_plus;rewrite > eq_minus_plus_plus_minus
+ [rewrite < minus_n_n;rewrite < plus_n_O;
+ rewrite > sym_plus;rewrite > sym_times;apply log_strano
+ [assumption
+ |lapply (leb_true_to_le ? ? H3);apply (trans_le ? ? ? H);
+ apply (le_exp_to_le1 ? ? 2);
+ [apply le_S_S;apply le_O_n
+ |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
+ apply lt_to_le;assumption]]
+ |apply le_n]
+ |rewrite > sym_times in \vdash (? (? % ?) ?);
+ rewrite > sym_times in \vdash (? (? ? %) ?);
+ rewrite < distr_times_plus;rewrite > sym_times;apply le_n]]
+ |apply (le_exp_to_le1 ? ? 2);
+ [apply le_S_S;apply le_O_n
+ |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
+ apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
+ apply le_n]]
+ |apply (trans_le ? (sigma_p n (λx:nat.leb (S n) (x*x)) (λi:nat.7*i/log b i*((2*(n!))/i))))
+ [apply le_sigma_p;intros;apply le_times_r;apply (trans_le ? (n!/i + n!/i))
+ [change in \vdash (? % ?) with (1 + n!/i);apply le_plus_l;
+ apply le_times_to_le_div
+ [generalize in match H3;cases i;simplify;intro
+ [destruct H4
+ |apply le_S_S;apply le_O_n]
+ |generalize in match H2;cases n;intro
+ [elim (not_le_Sn_O ? H4)
+ |change in \vdash (? ? %) with ((S n1)*(n1!));apply le_times
+ [apply lt_to_le;assumption
+ |apply lt_O_fact]]]
+ |rewrite > plus_n_O in \vdash (? (? ? %) ?);
+ change in \vdash (? % ?) with (2 * (n!/i));
+ apply le_times_div_div_times;
+ generalize in match H3;cases i;simplify;intro
+ [destruct H4
+ |apply le_S_S;apply le_O_n]]
+ |apply (trans_le ? (sigma_p n (\lambda x:nat.leb (S n) (x*x)) (\lambda i.((14*(n!))/log b i))))
+ [apply le_sigma_p;intros;
+ cut (b \leq i)
+ [|apply (le_exp_to_le1 ? ? 2);
+ [apply le_S_S;apply le_O_n
+ |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
+ apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
+ apply le_n]]
+ cut (1 < i)
+ [|apply (trans_le ? ? ? H Hcut)]
+ change in ⊢ (? ? (? % ?)) with ((7*2)*(n!));
+ rewrite > assoc_times in \vdash (? ? (? % ?));
+ apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?));
+ [apply lt_to_le;assumption
+ |rewrite > (eq_div_div_times ? ? 7)
+ [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
+ rewrite < assoc_times in \vdash (? (? % ?) ?);
+ apply (trans_le ? ? ? (le_div_times_m ? ? ? ? ?))
+ [apply lt_O_log
+ [apply lt_to_le;assumption
+ |assumption]
+ |unfold lt;rewrite > times_n_SO in \vdash (? % ?);
+ apply le_times;
+ [apply le_S_S;apply le_O_n
+ |apply lt_to_le;assumption]
+ |apply le_n]
+ |apply le_S_S;apply le_O_n
+ |apply lt_to_le;assumption]]
+ |apply (trans_le ? (sigma_p (S n) (\lambda x.leb (S n) (x*x))
+ (\lambda i.14*n!/log b i)))
+ [apply (bool_elim ? (leb (S n) (n*n)));intro
+ [rewrite > true_to_sigma_p_Sn
+ [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
+ apply le_plus_r;apply le_O_n
+ |assumption]
+ |rewrite > false_to_sigma_p_Sn
+ [apply le_n