+theorem teta_pi_p_teta: \forall m. teta (S (2*m))
+=pi_p (S (S (2*m))) (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)*teta (S m).
+intro.unfold teta.
+rewrite > (eq_pi_p1 ? (\lambda p.leb p (S m) \land primeb p) ? (\lambda p.p) (S(S m)))
+ [rewrite < (false_to_eq_pi_p (S(S m)) (S(S(2*m))))
+ [generalize in match (S(S(2*m))).intro.
+ elim n
+ [simplify.reflexivity
+ |apply (bool_elim ? (primeb n1));intro
+ [rewrite > true_to_pi_p_Sn
+ [apply (bool_elim ? (leb n1 (S m))); intro
+ [rewrite > false_to_pi_p_Sn
+ [rewrite > true_to_pi_p_Sn
+ [rewrite < assoc_times.
+ rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+ rewrite > assoc_times.
+ apply eq_f.
+ assumption
+ |apply true_to_true_to_andb_true;assumption
+ ]
+ |rewrite > lt_to_leb_false
+ [reflexivity
+ |apply le_S_S.
+ apply leb_true_to_le.
+ assumption
+ ]
+ ]
+ |rewrite > true_to_pi_p_Sn
+ [rewrite > false_to_pi_p_Sn
+ [rewrite > assoc_times.
+ apply eq_f.
+ assumption
+ |rewrite > H2.reflexivity
+ ]
+ |rewrite > H1.
+ rewrite > le_to_leb_true
+ [reflexivity
+ |apply not_le_to_lt.
+ apply leb_false_to_not_le.
+ assumption
+ ]
+ ]
+ ]
+ |assumption
+ ]
+ |rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_pi_p_Sn
+ [rewrite > false_to_pi_p_Sn
+ [assumption
+ |rewrite > H1.
+ rewrite > andb_sym.
+ reflexivity
+ ]
+ |rewrite > H1.
+ rewrite > andb_sym.
+ reflexivity
+ ]
+ |assumption
+ ]
+ ]
+ ]
+ |apply le_S_S.apply le_S_S.
+ apply le_times_n.
+ apply le_n_Sn
+ |intros.
+ rewrite > lt_to_leb_false
+ [reflexivity
+ |assumption
+ ]
+ ]
+ |intros.
+ rewrite > le_to_leb_true
+ [reflexivity
+ |apply le_S_S_to_le.
+ assumption
+ ]
+ |intros.reflexivity
+ ]
+qed.
+
+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_M_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.
+
+
+