+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