X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fchebyshev_thm.ma;fp=matita%2Flibrary%2Fnat%2Fchebyshev_thm.ma;h=129336d8e70fc15ac9d61f24d27cd5da6ccba153;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/library/nat/chebyshev_thm.ma b/matita/library/nat/chebyshev_thm.ma new file mode 100644 index 000000000..129336d8e --- /dev/null +++ b/matita/library/nat/chebyshev_thm.ma @@ -0,0 +1,953 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/neper.ma". + +definition C \def \lambda n.pi_p (S n) primeb + (\lambda p.match (leb (p*p) n) with + [ true => p + | false => S (n/p) ]). + +theorem asdasd : \forall n. exp n (prim n) \leq (A n)*(C n). +intro;unfold prim;rewrite < exp_sigma_p;unfold A;unfold C;rewrite < times_pi_p; +apply le_pi_p;intros; +apply (bool_elim ? (leb (i*i) n));intro + [change in \vdash (? ? (? ? %)) with i; + rewrite > sym_times;change in \vdash (? ? %) with (exp i (S (log i n))); + apply lt_to_le;apply lt_exp_log;apply prime_to_lt_SO; + apply primeb_true_to_prime;assumption + |change in \vdash (? ? (? ? %)) with (S (n/i)); + cut (log i n = S O) + [rewrite > Hcut;rewrite < exp_n_SO; + apply lt_to_le;rewrite > sym_times;apply lt_div_S;apply prime_to_lt_O; + apply primeb_true_to_prime;assumption + |apply antisymmetric_le + [apply le_S_S_to_le;apply not_le_to_lt;intro; + apply (leb_false_to_not_le ? ? H2);apply (trans_le ? (exp i (log i n))) + [rewrite < exp_SSO;apply le_exp; + [apply prime_to_lt_O; + apply primeb_true_to_prime;assumption + |assumption] + |apply le_exp_log;apply (trans_le ? i) + [apply prime_to_lt_O;apply primeb_true_to_prime;assumption + |apply le_S_S_to_le;assumption]] + |apply (trans_le ? (log i i)) + [rewrite > log_n_n; + [apply le_n + |apply prime_to_lt_SO;apply primeb_true_to_prime;assumption] + |apply le_log + [apply prime_to_lt_SO;apply primeb_true_to_prime;assumption + |apply le_S_S_to_le;assumption]]]]] +qed. + +definition theta_pi \def + \lambda n.pi_p (S n) primeb (\lambda p.p). + +definition C1 \def + \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (x*x) n)) (\lambda p.p). + +definition C2 \def + \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (S n) (x*x))) (\lambda p.S (n/p)). + + +theorem jj : \forall n.C n = C1 n * C2 n. +intro;unfold C;unfold C1;unfold C2; +cut (\forall m.pi_p (S n) primeb +(λp:nat + .match leb (p*p) m in bool return λb:bool.nat with  + [true⇒p|false⇒S (m/p)]) +=pi_p (S n) (λx:nat.primeb x∧leb (x*x) m) (λp:nat.p) + *pi_p (S n) (λx:nat.primeb x∧leb (S m) (x*x)) (λp:nat.S (m/p))) + [apply Hcut; + |intro;elim n 0 + [simplify;reflexivity + |intro;apply (bool_elim ? (primeb (S n1))) + [intros;rewrite > true_to_pi_p_Sn + [apply (bool_elim ? (leb ((S n1)*(S n1)) m)) + [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;rewrite < assoc_times;reflexivity + |rewrite > H;lapply (leb_true_to_le ? ? H2); + lapply (le_to_not_lt ? ? Hletin); + apply (bool_elim ? (leb (S m) (S n1 * S n1))) + [intro;apply False_ind;apply Hletin1; + apply leb_true_to_le;assumption + |intro;reflexivity]] + |rewrite > H2;rewrite > H;reflexivity] + |intro;rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;rewrite < assoc_times; + rewrite > sym_times in \vdash (? ? (? % ?) ?); + rewrite > assoc_times;reflexivity + |rewrite > H; + change in \vdash (? ? % ?) with (leb (S m) (S n1* S n1)); + apply le_to_leb_true;apply not_le_to_lt; + apply leb_false_to_not_le;assumption] + |rewrite > H;rewrite > H2;reflexivity]] + |assumption] + |intros;rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;reflexivity + |rewrite > H;elim (leb (S m) (S n1*S n1));simplify;reflexivity] + |rewrite > H;elim (leb (S n1*S n1) m);simplify;reflexivity] + |assumption]]]] +qed. + +theorem log_pi_p : \forall n,b,f,g.S O < b \to + log b (pi_p n f g) \leq + (sigma_p n f (\lambda x.S O)) + (sigma_p n f (\lambda x.log b (g x))). +intros;elim n + [simplify;rewrite < times_n_SO;apply (leb_elim b (S O)) + [intro;elim (lt_to_not_le ? ? H);assumption + |intro;simplify;apply le_n] + |apply (bool_elim ? (f n1)) + [intro;rewrite > true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [apply (trans_le ? (S ((log b (g n1)) + (log b (pi_p n1 f g))))) + [apply log_times;assumption + |rewrite > assoc_plus; + change in \vdash (? ? %) with (S (sigma_p n1 f (\lambda x.S O)+(log b (g n1)+sigma_p n1 f (\lambda x.log b (g x))))); + apply le_S_S;rewrite < assoc_plus; + rewrite > sym_plus in \vdash (? ? (? % ?)); + rewrite > assoc_plus;apply le_plus; + [apply le_n]]]]] + assumption + |intro;rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn]] + assumption]] +qed. + +axiom daemon : False. +(* +lemma lt_log_to_lt : \forall b,m,n.S O < b \to log b m < log b n \to m < n. +intros;apply not_le_to_lt;intro;elim (le_to_not_lt ? ? (le_log ? ? ? H H2)); +assumption. +qed. + +theorem ababbs: \forall n,a,b.S O < b \to O < n \to n < exp b a \to log b n < a. +intros;unfold log;apply not_le_to_lt;intro;apply (lt_to_not_le ? ? H2); +elim (le_to_or_lt_eq ? ? H3) + [apply lt_to_le;apply (lt_log_to_lt b ? ? H);rewrite > eq_log_exp;assumption + |apply (trans_le ? (exp b (log b n))) + [rewrite < H4;apply le_n + |apply le_exp_log;assumption]] +qed. + +theorem exp_exp_to_log : \forall b,n,k.S O < b \to +exp b k \leq n \to n < exp b (S k) \to log b n = k. +intros;unfold log;lapply (ababbs ? ? ? H ? H2) + [apply (trans_le ? ? ? ? H1);apply lt_O_exp + |unfold log in Hletin;lapply (le_to_leb_true ? ? H1); + lapply (f_m_to_le_max (λx:nat.leb ((b)\sup(x)) n) n ? ? Hletin1) + [ + elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? Hletin)) + [unfold log in H3; +]]elim daemon. +qed. + +theorem xxx_log : \forall a,b.S O < b \to O < a \to log b (b*a) = S (log b a). +intros 3;elim a + [elim (not_le_Sn_O ? H1); + |apply (inj_exp_r b) + [assumption + |*) + +theorem le_log_C2_sigma_p : \forall n,b. S O < b \to +log b (C2 n) \leq +(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) + +(prim n + (((sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i.prim i * S (n!/i))) + *(S (log b 3)))/n!)). +intros;unfold C2; +apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1) ++sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) + (λi.log b (S (n/i))))) + [apply log_pi_p;assumption + |apply le_plus + [apply le_n + |apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λi:nat.S (log b (n/i))))) + [apply le_sigma_p;intros;cut (log b (b*(n/i)) = S (log b (n/i))) + [rewrite < Hcut;apply le_log + [assumption + |elim H + [rewrite < times_SSO_n;change in \vdash (? % ?) with (S O + (n/i)); + apply le_plus; + [apply le_times_to_le_div + [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))); + |rewrite < times_n_SO;apply le_S_S_to_le;assumption] + |apply le_n] + |apply (trans_le ? ? ? H4);apply le_times_l;apply le_S;apply le_n]] + |rewrite > exp_n_SO in ⊢ (? ? (? ? (? % ?)) ?); + rewrite > log_exp; + [reflexivity + |assumption + |apply le_times_to_le_div; + [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))); + |rewrite < times_n_SO;apply le_S_S_to_le;assumption]]] + |change in ⊢ (? (? ? ? (λi:?.%)) ?) with ((S O) + (log b (n/i))); + rewrite > (sigma_p_plus_1 ? (\lambda x.S O)); + apply le_plus + [unfold prim;apply le_sigma_p1;intros;elim (leb (S n) (i*i)); + [rewrite > andb_sym;apply le_n + |rewrite > andb_sym;apply le_O_n] + |apply sigma_p_log_div;assumption]]]] +qed. +(* + +lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to +prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n). +(* la stima del secondo addendo è ottenuta considerando che + logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *) +intros;apply le_times_to_le_div; + [apply lt_O_log; + [apply (trans_le ? b) + [apply lt_to_le;assumption + |assumption] + |assumption] + |apply (trans_le ? (log b (exp n (prim n)))) + [rewrite > sym_times;apply log_exp2 + [assumption + |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption] + |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O))))) + *(exp (S (S O)) ((S (S (S (S O))))*n))))) + [apply le_log + [assumption + |apply le_exp_primr;apply (trans_le ? ? ? H H1)] + |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) + + (log b (exp (S (S O)) ((S (S (S (S O))))*n)))))) + [apply log_times;assumption + |apply le_S_S;apply le_plus + [apply log_exp1;assumption + |cases H + [rewrite > times_n_SO in \vdash (? (? ? %) ?); + rewrite > log_exp + [rewrite < plus_n_O;apply le_n + |apply le_n + |apply le_n] + |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O)))))) + [apply log_exp1;apply le_S;assumption + |rewrite > times_n_SO in \vdash (? ? %); + apply le_times_r;apply le_S_S; + rewrite > lt_to_log_O + [apply le_n + |apply lt_O_S + |apply le_S_S;assumption]]]]]]]] +qed. + +theorem le_log_C2_stima : \forall n,b. S O < b \to b*b < n \to +log b (C2 n) \leq +(*(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +*) +((S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n)) + +(((S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n)) + + (((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))) + *(S (log b (S (S (S O))))))/n!)).intros. +apply (trans_le ? ? ? (le_log_C2_sigma_p ? ? ?)) + [assumption + |apply le_plus + [apply (trans_le ? ? ? ? (le_prim_n_stima ? ? ? ?)); + [unfold prim;apply le_sigma_p1;intros; + do 2 rewrite < times_n_SO;elim (primeb i) + [elim (leb (S n) (i*i));simplify [apply le_n|apply le_O_n] + |simplify;apply le_n] + |assumption + |apply (trans_le ? ? ? ? H1);apply le_S;apply le_times_n; + apply lt_to_le;assumption] + |apply le_plus + [apply le_prim_n_stima; + [assumption + |apply (trans_le ? (b*b)) + [apply le_times_n;apply lt_to_le;assumption + |apply lt_to_le;assumption]] + |apply monotonic_div + [apply lt_O_fact + |apply le_times_l;apply le_sigma_p;intros;apply le_times_l; + apply le_prim_n_stima + [assumption + |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. + +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 + |assumption]] + |apply (trans_le ? ? ? (le_sigma_p_div_log_div_pred_log ? ? ? ? ?)); + [assumption + |apply lt_to_le;assumption + |rewrite < assoc_times; + rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?); + rewrite < assoc_times;apply le_n]]]]] +qed. + +theorem le_log_C2_stima2 : \forall n,b. S O < b \to b*b < n \to +log b (C2 n) \leq +(14*n/(log b n)) + + ((((28*n*n!)/pred (log b n)) + *(S (log b (S (S (S O))))))/n!).intros. +apply (trans_le ? ? ? (le_log_C2_stima ? ? H H1)); +rewrite < assoc_plus in \vdash (? % ?);apply le_plus + [rewrite > times_SSO_n in \vdash (? % ?); + apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?)) + [apply lt_O_log + [apply (trans_le ? (b*b)) + [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption + |apply lt_to_le;assumption] + |apply (trans_le ? (b*b)) + [rewrite > times_n_SO in \vdash (? % ?);apply le_times + [apply le_n|apply lt_to_le;assumption] + |apply lt_to_le;assumption]] + |change in \vdash (? ? (? (? % ?) ?)) with (2*7); + apply monotonic_div; + [apply lt_O_log + [apply (trans_le ? (b*b)) + [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption + |apply lt_to_le;assumption] + |apply (trans_le ? (b*b)) + [rewrite > times_n_SO in \vdash (? % ?);apply le_times + [apply le_n|apply lt_to_le;assumption] + |apply lt_to_le;assumption]] + |rewrite > assoc_times;apply le_times_r; + change in \vdash (? (? (? (? ? %) ?)) ?) with (1 + (log b (pred n))); + rewrite > distr_times_plus; + change in \vdash (? % ?) with (1 + (4*1+4*log b (pred n)+4*n)); + do 2 rewrite < assoc_plus;simplify in ⊢ (? (? (? % ?) ?) ?); + change in ⊢ (? ? %) with ((3+4)*n);rewrite > sym_times in \vdash (? ? %); + rewrite > distr_times_plus; + rewrite > sym_times in \vdash (? ? (? % ?)); + rewrite > sym_times in \vdash (? ? (? ? %)); + apply le_plus_l;rewrite > sym_plus;apply log_strano + [assumption + |apply (trans_le ? ? ? H);apply (trans_le ? (b*b)) + [rewrite > times_n_SO in \vdash (? % ?); + apply le_times_r;apply lt_to_le;assumption + |apply lt_to_le;assumption]]]] + |apply monotonic_div + [apply lt_O_fact + |apply le_times_l;apply (le_sigma_p_lemma1 ? ? H H1)]] +qed. + +theorem le_log_C2_stima3 : \forall n,b. S O < b \to b*b < n \to +log b (C2 n) \leq +(14*n/(log b n)) + + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n)).intros. +apply (trans_le ? ? ? (le_log_C2_stima2 ? ? H H1));apply le_plus_r; +(*apply (trans_le ? ((28*n)*(28*n*n!/pred (log b n)*S (log b 3)/(28*n*n!)))) + [*) +rewrite > (eq_div_div_times ? ? (28*n)) in \vdash (? % ?) + [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?); + rewrite < assoc_times; + apply le_div_times_m; + [apply (trans_le ? (pred (log b (b*b)))) + [rewrite < exp_SSO;rewrite > eq_log_exp; + [apply le_n + |assumption] + |rewrite < exp_SSO;rewrite > eq_log_exp; + [simplify;rewrite > minus_n_O in \vdash (? ? (? %)); + rewrite < eq_minus_S_pred; + apply le_plus_to_minus_r;simplify; + rewrite < (eq_log_exp b 2); + [apply le_log + [assumption + |rewrite > exp_SSO;apply lt_to_le;assumption] + |assumption] + |assumption]] + |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times + [rewrite > times_n_SO in \vdash (? % ?);apply le_times + [apply le_S_S;apply le_O_n + |apply (trans_le ? ? ? ? H1);apply le_S_S; + rewrite > times_n_SO;apply le_times + [apply le_O_n + |apply lt_to_le;assumption]] + |apply lt_O_fact]] + |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times + [apply le_S_S;apply le_O_n + |apply (trans_le ? ? ? ? H1);apply le_S_S; + rewrite > times_n_SO;apply le_times + [apply le_O_n + |apply lt_to_le;assumption]] + |apply lt_O_fact] +qed. + +lemma le_prim_log1: \forall n,b. S O < b \to O < n \to + (prim n)*(log b n) \leq + log b (A n) + log b (C1 n) + log b (C2 n) + 2. +intros.change in \vdash (? ? (? ? %)) with (1+1). +rewrite < assoc_plus;rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)). +rewrite > assoc_plus in ⊢ (? ? (? % ?)); +apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1)); + [apply (trans_le ? (log b (A n * (C1 n * C2 n)))) + [apply (trans_le ? (log b (exp n (prim n)))) + [apply log_exp2;assumption + |apply le_log + [assumption + |rewrite < jj;apply asdasd]] + |rewrite > sym_plus;simplify;apply log_times;assumption] + |apply le_plus_l;apply le_plus_r;rewrite > sym_plus;simplify;apply log_times; + assumption] +qed. + +lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to + log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1. +intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n)))))) + [apply le_log + [assumption + |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption] + |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n))))))); + [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n))))); + apply log_times;assumption + |apply le_plus_r;apply le_plus;apply log_exp1;assumption]] +qed. + +lemma le_theta_pi_A : \forall n.theta_pi n \leq A n. +intro.unfold theta_pi.unfold A.apply le_pi_p.intros. +rewrite > exp_n_SO in \vdash (? % ?). +cut (O < i) + [apply le_exp + [assumption + |apply lt_O_log + [apply (trans_le ? ? ? Hcut);apply le_S_S_to_le;assumption + |apply le_S_S_to_le;assumption]] + |apply prime_to_lt_O;apply primeb_true_to_prime;assumption] +qed. + +definition sqrt \def + \lambda n.max n (\lambda x.leb (x*x) n). + +theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m. +intros;apply (trans_le ? (sqrt m * sqrt m)) + [apply le_times;assumption + |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m); + apply (ex_intro ? ? O);split + [apply le_O_n + |simplify;reflexivity]] +qed. + +theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m. +intros;apply (trans_le ? (sqrt m * sqrt m)) + [apply (trans_le ? (S n * S n)) + [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n)) + [apply le_times_r;apply le_S;apply le_n + |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?); + apply le_plus_r;apply le_O_n] + |apply le_times;assumption] + |apply le_sqrt_to_le_times_l;apply le_n] +qed. + +theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n. +intros;apply not_le_to_lt;intro; +apply ((leb_false_to_not_le ? ? + (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?)) + H1); +apply (trans_le ? ? ? ? H1);cases n + [apply le_n + |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times + [apply le_S_S;apply le_O_n + |apply le_n]] +qed. + +theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n. +intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n)) + [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n) + [simplify;reflexivity + |apply (bool_elim ? (primeb (S n1))) + [intro;rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %) + [apply eq_f2 + [reflexivity + |apply H;intros;apply H1;apply le_S;assumption] + |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n)); + rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n] + |assumption] + |intro;rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %) + [apply H;intros;apply H1;apply le_S;assumption + |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n)); + rewrite > H2;whd;reflexivity] + |assumption]]] + |apply le_S_S;unfold sqrt;apply le_max_n + |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify + [rewrite > lt_to_leb_false + [reflexivity + |apply le_sqrt_to_le_times_r;assumption] + |reflexivity]] +qed. + +lemma le_sqrt_n_n : \forall n.sqrt n \leq n. +intro.unfold sqrt.apply le_max_n. +qed. + +lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to + (prim n)*(log b n) \leq + 2*S (log b (pred n))+2*(pred n)*S (log b 2) + +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) + +(14*n/log b n+28*n*S (log b 3)/pred (log b n)) + +4. +intros.cut (1 < n) + [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) + + (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) + + ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2)) + [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?)) + [apply lt_to_le;assumption + |apply le_plus_l;apply le_plus + [apply le_plus + [apply le_log_A1;assumption + |rewrite < eq_theta_pi_sqrt_C1;apply (trans_le ? (log b (A (sqrt n)))) + [apply le_log + [assumption + |apply le_theta_pi_A] + |apply le_log_A1 + [assumption + |apply (trans_le ? ? ? H);apply lt_to_le;assumption]]] + |apply le_log_C2_stima3; + [assumption + |apply lt_sqrt_to_le_times_l;assumption]]] + |rewrite > assoc_plus in ⊢ (? (? % ?) ?); + rewrite > sym_plus in ⊢ (? (? (? ? %) ?) ?); + rewrite > assoc_plus in \vdash (? % ?); + rewrite > assoc_plus in ⊢ (? (? ? %) ?); + rewrite > assoc_plus in ⊢ (? (? % ?) ?); + rewrite > assoc_plus in \vdash (? % ?); + rewrite < assoc_plus in ⊢ (? (? ? %) ?); + rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?); + rewrite > sym_plus in ⊢ (? (? ? (? (? ? %) ?)) ?); + rewrite < assoc_plus in ⊢ (? (? ? (? % ?)) ?); + rewrite < assoc_plus in \vdash (? % ?); + rewrite < assoc_plus in ⊢ (? (? % ?) ?); + rewrite > assoc_plus in \vdash (? % ?); + rewrite > sym_plus in ⊢ (? (? ? %) ?); + rewrite > assoc_plus in ⊢ (? (? ? %) ?); + rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?); + rewrite > assoc_plus in ⊢ (? (? ? %) ?); + rewrite > assoc_plus in ⊢ (? (? ? (? ? %)) ?); + simplify in ⊢ (? (? ? (? ? (? ? %))) ?); + rewrite < assoc_plus in ⊢ (? (? ? %) ?); + rewrite < assoc_plus in ⊢ (? % ?);apply le_plus_l; + rewrite > assoc_plus in \vdash (? % ?); + rewrite > assoc_plus in ⊢ (? (? ? %) ?); + rewrite > sym_plus in ⊢ (? (? ? (? ? %)) ?); + rewrite < assoc_plus in ⊢ (? (? ? %) ?); + rewrite < assoc_plus in \vdash (? % ?);apply le_plus_l; + rewrite > assoc_plus in \vdash (? ? %);apply le_n] + |apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1); + apply le_sqrt_n_n] +qed. + +lemma eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c). +intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?) + [rewrite > (div_mod (a \mod (b*c)) b) + [rewrite < assoc_plus; + rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?); + rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?); + rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?); + rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?); + rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?); + rewrite > (div_plus_times b) + [rewrite > (div_plus_times c) + [reflexivity + |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %); + apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption] + |apply lt_mod_m_m;assumption] + |assumption] + |unfold lt;rewrite > times_n_SO;apply le_times;assumption] +qed. + +lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to + (prim n) \leq + 2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n) + +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n) + + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n) + +4/(log b n) + 6. +intros; +cut (O < log b n) + [|apply lt_O_log; + [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n)) + [apply lt_to_le;assumption + |apply le_sqrt_n_n;] + |apply (trans_le ? (sqrt n)) + [apply lt_to_le;assumption + |apply le_sqrt_n_n]]] +apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2) + +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) + +(14*n/log b n+28*n*S (log b 3)/pred (log b n)) + +4)/(log b n))) + [apply le_times_to_le_div + [assumption + |rewrite > sym_times;apply le_prim_log_stima;assumption] + |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2) ++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) ++(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?)) + [assumption + |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %); + rewrite > sym_plus in \vdash (? ? (? ? %)); + rewrite < assoc_plus in \vdash (? ? %); + apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2) ++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?)); + [assumption + |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S; + change in \vdash (? ? (? ? %)) with (1+3); + rewrite < assoc_plus in \vdash (? ? %); + rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)); + rewrite > assoc_plus in ⊢ (? ? (? % ?)); + rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %); + rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus + [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*pred n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*pred (sqrt n)*S (log b 2)) (log b n) ?)) + [assumption + |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1); + rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)); + rewrite > assoc_plus in ⊢ (? ? (? % ?)); + rewrite > sym_plus in \vdash (? ? %); + rewrite < assoc_plus in \vdash (? ? %); + rewrite > sym_plus in \vdash (? ? (? % ?)); + apply le_plus + [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S; + assumption + |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S; + assumption]] + |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?)); + [assumption + |apply le_S_S;apply le_plus + [rewrite > eq_div_div_div_times; + [apply le_n + |*:assumption] + |rewrite > eq_div_div_div_times + [apply le_n + |rewrite > minus_n_O in \vdash (? ? (? %)); + rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus; + apply (trans_le ? (log b (sqrt n * sqrt n))) + [elim daemon; + |apply le_log; + [assumption + |elim daemon]] + |assumption]]]]]]] +qed. + +lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n. +intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O); +split + [apply le_O_n + |simplify;reflexivity] +qed. + +lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n. +intros. +apply (trans_le ? ? ? ? (leq_sqrt_n ?)); +apply le_times_r;unfold sqrt; +apply f_m_to_le_max + [apply le_log_n_n;apply lt_to_le;assumption + |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n)) + [apply (trans_le ? (exp b (log b n))) + [elim (log b n) + [apply le_O_n + |simplify in \vdash (? ? %); + elim (le_to_or_lt_eq ? ? (le_O_n n1)) + [elim (le_to_or_lt_eq ? ? H3) + [apply (trans_le ? (3*(n1*n1))); + [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?); + simplify in \vdash (? % ?); + simplify;rewrite > sym_plus; + rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?); + rewrite > assoc_plus;apply le_plus_r; + rewrite < plus_n_Sm; + rewrite < plus_n_O; + apply lt_plus;rewrite > times_n_SO in \vdash (? % ?); + apply lt_times_r1;assumption; + |apply le_times + [assumption + |assumption]] + |rewrite < H4;apply le_times + [apply lt_to_le;assumption + |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]] + |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]] + |simplify;apply le_exp_log;assumption] + |rewrite < H1;simplify;apply le_n]] +qed. + +(* Bertrand weak, lavori in corso + +theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n). +intros. +apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?))) + [apply le_n + |unfold sqrt;apply f_m_to_le_max + [do 6 apply lt_to_le;assumption + |apply le_to_leb_true;assumption] + |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n)) + [|apply le_S_S_to_le;rewrite < S_pred + [apply le_times_to_le_div2 + [apply lt_O_S + |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n); + rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %)))); + rewrite > sym_times in \vdash (? ? %); + apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?); + apply lt_times; + [apply lt_O_S + |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]] + |apply le_times_to_le_div; + [apply lt_O_S + |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n))))) + [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n + |change in \vdash (? % ?) with (4 + log 2 n); + rewrite > S_pred in \vdash (? ? (? ? %)); + [change in ⊢ (? ? (? ? %)) with (1 + pred n); + rewrite > distr_times_plus;apply le_plus_r;elim H + [simplify;do 3 apply le_S_S;apply le_O_n + |apply (trans_le ? (log 2 (2*n1))) + [apply le_log; + [apply le_S_S;apply le_n + |rewrite < times_SSO_n; + change in \vdash (? % ?) with (1 + n1); + apply le_plus_l;apply (trans_le ? ? ? ? H1); + apply lt_O_S] + |apply (trans_le ? (S (4*pred n1))) + [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?); + rewrite > log_exp + [change in \vdash (? ? %) with (1 + (4*pred n1)); + apply le_plus_r; + assumption + |apply le_S_S;apply le_n + |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n] + |simplify in \vdash (? ? (? ? %)); + rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?); + rewrite < eq_minus_S_pred; + rewrite > distr_times_minus; + change in \vdash (? % ?) with (1 + (4*n1 - 4)); + rewrite > eq_plus_minus_minus_minus + [simplify;apply le_minus_m; + |apply lt_O_S + |rewrite > times_n_SO in \vdash (? % ?); + apply le_times_r;apply (trans_le ? ? ? ? H1); + apply lt_O_S]]]] + |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]] + apply (trans_le ? ? ? ? Hcut); +*) +*) \ No newline at end of file