proposition: Lemma divp_mulA d p q : d %| q -> p * (q %/ d) = p * q %/ d.
proof: Proof. case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite !divp0 mulr0. by apply: IdomainUnit.divp_mulA; rewrite unitfE lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)