proposition: Lemma eqpf_eq p q : reflect (exists2 c, c != 0 & p = c *: q) (p %= q).
proof: Proof. apply: (iffP idP); last first. case=> c nz_c ->; apply/eqpP. by exists (1, c); rewrite ?scale1r ?oner_eq0. have [->|nz_q] := eqVneq q 0. by rewrite eqp0=> /eqP ->; exists 1; rewrite ?scale1r ?oner_eq0. case/IdomainUnit.ulc_eqpP; first by rewrite unitfE lead_coef_eq0. by move=> c nz_c ->; exists c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)