proposition: Lemma divp_eq0 p q : (p %/ q == 0) = [|| p == 0, q ==0 | size p < size q].
proof: Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. case: eqVneq => // _; case: eqVneq => // qn0. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)