[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)).