proposition: Lemma eq_dvdp c quo q p : c != 0 -> c *: p = quo * q -> q %| p.
proof: Proof. move=> cn0; case: (eqVneq p 0) => [->|nz_quo def_quo] //. pose p1 : {poly R} := lead_coef q ^+ scalp p q *: quo - c *: (p %/ q). have E1: c *: (p %% q) = p1 * q. rewrite mulrDl mulNr -scalerAl -def_quo scalerA mulrC -scalerA. by rewrite -scalerAl -scalerBr divp_eq addrAC subrr add0r. rewrite /dvdp; apply/idPn=> m_nz. have: p1 * q != 0 by rewrite -E1 -mul_polyC mulf_neq0 // polyC_eq0. rewrite mulf_eq0; case/norP=> p1_nz q_nz. have := ltn_modp p q; rewrite q_nz -(size_scale (p %% q) cn0) E1. by rewrite size_mul // polySpred // ltnNge leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)