proposition: Lemma dvdpP q p : reflect (exists2 cqq, cqq.1 != 0 & cqq.1 *: p = cqq.2 * q) (q %| p).
proof: Proof. rewrite dvdp_eq; apply: (iffP eqP) => [e | [[c qq] cn0 e]]. by exists (lead_coef q ^+ scalp p q, p %/ q) => //=. apply/eqP; rewrite -dvdp_eq dvdpE. have Ecc: c%:P != 0 by rewrite polyC_eq0. have [->|nz_p] := eqVneq p 0; first by rewrite rdvdp0. pose p1 : {poly R} := lead_coef q ^+ rscalp p q *: qq - c *: (rdivp p q). have E1: c *: rmodp p q = p1 * q. rewrite mulrDl mulNr -scalerAl -e scalerA mulrC -scalerA -scalerAl. by rewrite -scalerBr rdivp_eq addrC addKr. suff: p1 * q == 0 by rewrite -E1 -mul_polyC mulf_eq0 (negPf Ecc). rewrite mulf_eq0; apply/norP; case=> p1_nz q_nz; have:= ltn_rmodp p q. by rewrite q_nz -(size_scale _ cn0) E1 size_mul // polySpred // ltnNge leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)