proposition: Lemma divpKC d p : d %| p -> d * (p %/ d) = (lead_coef d ^+ scalp p d) *: p.
proof: Proof. by move=> ?; rewrite mulrC divpK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)