include "nat/pi_p.ma".
include "nat/factorization.ma".
include "nat/factorial2.ma".
+include "nat/o.ma".
definition prim: nat \to nat \def
\lambda n. sigma_p (S n) primeb (\lambda p.1).
rewrite < plus_n_O.
rewrite > exp_plus_times.
apply le_times_l.
- alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con".
apply le_times_SSO_n_exp_SSO_n
]
|apply le_times_to_le_div2