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