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