proposition: Lemma modpZl c p : (c *: p) %% d = c *: (p %% d).
proof: Proof. have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r mod0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). by rewrite -scalerAl -scalerDr -divp_eq. suff s: size (c *: (p %% d)) < size d by case: (edivpP e s) => _ ->. rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)