proposition: Lemma dvdp_addr m d n : d %| m -> (d %| m + n) = (d %| n).
proof: Proof. case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite add0r. 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. move/eqP=> Eq2; apply: (@eq_dvdp _ (c1 *: q2 - c2 *: q1) _ _ sn0). rewrite mulrDl -scaleNr -!scalerAl -Eq1 -Eq2 !scalerA. by rewrite mulNr mulrC scaleNr -scalerBr addrC addKr. have sn0 : c1 * c2 != 0. by rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 (negPf dn0) andbF. move/eqP=> Eq2; apply: (@eq_dvdp _ (c1 *: q2 + c2 *: q1) _ _ sn0). by rewrite mulrDl -!scalerAl -Eq1 -Eq2 !scalerA mulrC addrC scalerDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)