[apply (bool_elim ? (leb ((S n1)*(S n1)) m))
[intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
[rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
- [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+ [rewrite > H1;rewrite < assoc_times;reflexivity
|rewrite > H;lapply (leb_true_to_le ? ? H2);
lapply (le_to_not_lt ? ? Hletin);
apply (bool_elim ? (leb (S m) (S n1 * S n1)))