proposition: Lemma dvdp_eq q p : (q %| p) = (lead_coef q ^+ scalp p q *: p == (p %/ q) * q).
proof: Proof. rewrite dvdpE rdvdp_eq scalpE divpE; case: ifP => ulcq //. rewrite expr0 scale1r -scalerAl; apply/eqP/eqP => [<- | {2}->]. by rewrite scalerA mulVr ?scale1r // unitrX. by rewrite scalerA mulrV ?scale1r // unitrX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)