+theorem div_teta_teta: \forall m.
+teta (S(2*m))/teta (S m) = pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p).
+intros.apply (div_mod_spec_to_eq ? ? ? ? ? O (div_mod_spec_div_mod ? ? ? ))
+ [apply lt_O_teta
+ |apply div_mod_spec_intro
+ [apply lt_O_teta
+ |rewrite < plus_n_O.
+ apply teta_pi_p_teta
+ ]
+ ]
+qed.
+
+theorem le_teta_M_teta: \forall m.
+teta (S(2*m)) \le (M m)*teta (S m).
+intro.
+rewrite > teta_pi_p_teta.
+apply le_times_l.
+apply divides_to_le
+ [unfold M.apply lt_O_bc.apply lt_to_le.
+ apply le_S_S.apply le_times_n.
+ apply le_n_Sn
+ |apply divides_pi_p_M
+ ]
+qed.
+
+theorem lt_O_to_le_teta_exp_teta: \forall m. O < m\to
+teta (S(2*m)) < exp 2 (2*m)*teta (S m).
+intros.
+apply (le_to_lt_to_lt ? (M m*teta (S m)))
+ [apply le_teta_M_teta
+ |apply lt_times_l1
+ [apply lt_O_teta
+ |apply lt_M.
+ assumption
+ ]
+ ]
+qed.
+
+theorem teta_pred: \forall n. S O < n \to teta (2*n) = teta (pred (2*n)).
+intros.unfold teta.
+rewrite > false_to_pi_p_Sn
+ [rewrite < S_pred
+ [reflexivity
+ |rewrite > (times_n_O 2) in ⊢ (? % ?).
+ apply lt_times_r.
+ apply lt_to_le.assumption
+ ]
+ |apply not_prime_to_primeb_false.
+ intro.
+ elim H1.
+ apply (lt_to_not_eq ? ? H).
+ apply (injective_times_r 1).
+ rewrite < times_n_SO.
+ apply H3
+ [apply (witness ? ? n).reflexivity
+ |apply le_n
+ ]
+ ]
+qed.
+
+theorem le_teta: \forall m.teta m \le exp 2 (2*m).
+intro.apply (nat_elim1 m).intros.
+elim (or_eq_eq_S m1).
+elim H1
+ [rewrite > H2.
+ generalize in match H2.
+ cases a
+ [intro.apply le_n
+ |cases n;intros
+ [apply leb_true_to_le.reflexivity
+ |rewrite > teta_pred
+ [rewrite > times_SSO.
+ change in ⊢ (? (? %) ?) with (S (2*S n1)).
+ apply (trans_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
+ [apply lt_to_le.
+ apply lt_O_to_le_teta_exp_teta.
+ apply lt_O_S
+ |rewrite < times_SSO.
+ change in ⊢ (? ? (? ? %)) with ((2*S (S n1))+((2*S (S n1)) + O)).
+ rewrite < plus_n_O.
+ rewrite > exp_plus_times.
+ apply le_times
+ [apply le_exp
+ [apply lt_O_S
+ |apply le_times_r.
+ apply le_n_Sn
+ ]
+ |apply H.
+ rewrite > H3.
+ apply lt_m_nm
+ [apply lt_O_S
+ |apply le_n
+ ]
+ ]
+ ]
+ |apply le_S_S.apply lt_O_S
+ ]
+ ]
+ ]
+ |rewrite > H2.
+ generalize in match H2.
+ cases a;intro
+ [apply leb_true_to_le.reflexivity
+ |apply (trans_le ? (exp 2 (2*(S n))*teta (S (S n))))
+ [apply lt_to_le.
+ apply lt_O_to_le_teta_exp_teta.
+ apply lt_O_S
+ |change in ⊢ (? ? (? ? %)) with (S (2*S n) + (S (2*S n) +O)).
+ rewrite < plus_n_O.
+ rewrite < plus_n_Sm.
+ rewrite < sym_plus.
+ rewrite > plus_n_Sm.
+ rewrite > exp_plus_times.
+ apply le_times_r.
+ rewrite < times_SSO.
+ apply H.
+ rewrite > H3.
+ apply le_S_S.
+ apply lt_m_nm
+ [apply lt_O_S
+ |apply le_n
+ ]
+ ]
+ ]
+ ]
+qed.
+
+(*
+alias id "sqrt" = "cic:/matita/nat/sqrt/sqrt.con".
+alias id "not" = "cic:/matita/logic/connectives/Not.con".
+theorem absurd_bound: \forall n. exp 2 7 \le n \to
+(\forall p. n < p \to p < 2*n \to not (prime p)) \to
+bc (2*n) n < exp (2*n) (div (sqrt (2*n)) 2 - 1)*exp 4 (div (2*n) 3).
+intros.
+cut (O < n)
+ [cut (sqrt (2*n) < div (2*n) 3)
+ [
+ |
+*)
+