proposition: Lemma dvdp_eq_div p q : d %| p -> (q == p %/ d) = (q * d == p).
proof: Proof. move/divpK=> {2}<-; apply/eqP/eqP; first by move->. apply/mulIf; rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->. by rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)