(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/chebyshev_teta".
-
include "nat/binomial.ma".
include "nat/pi_p.ma".
[unfold bc.rewrite > H3.
rewrite > sym_times.
rewrite > lt_O_to_div_times
- [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2)
+ [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n1)
[apply False_ind.
elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
[apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).