proposition: Lemma dvdp_eq q p : (q %| p) = (p == p %/ q * q).
proof: Proof. have [-> | qn0] := eqVneq q 0; first by rewrite dvd0p mulr0 eq_sym. by apply: IdomainUnit.dvdp_eq; rewrite unitfE lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)