+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)
+ [
+ |
+*)