proposition: Lemma dvdp_mod d n m : d %| n -> (d %| m) = (d %| m %% n).
proof: Proof. have [-> | nn0] := eqVneq n 0; first by rewrite modp0. case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite modp0. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Eq1. apply/idP/idP; rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _. have sn0 : c1 * c2 != 0. by rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 (negPf dn0) andbF. pose quo := (c1 * lead_coef n ^+ scalp m n) *: q2 - c2 *: (m %/ n) * q1. move/eqP=> Eq2; apply: (@eq_dvdp _ quo _ _ sn0). rewrite mulrDl mulNr -!scalerAl -!mulrA -Eq1 -Eq2 -scalerAr !scalerA. rewrite mulrC [_ * c2]mulrC mulrA -[((_ * _) * _) *: _]scalerA -scalerBr. by rewrite divp_eq addrC addKr. have sn0 : c1 * c2 * lead_coef n ^+ scalp m n != 0. rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 ?(negPf dn0) ?andbF //. by rewrite (negPf nn0) andbF. move/eqP=> Eq2; apply: (@eq_dvdp _ (c2 *: (m %/ n) * q1 + c1 *: q2) _ _ sn0). rewrite -scalerA divp_eq scalerDr -!scalerA Eq2 scalerAl scalerAr Eq1. by rewrite scalerAl mulrDl mulrA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)