proposition: Lemma modpZr c p d : c != 0 -> p %% (c *: d) = (p %% d).
proof: Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). by rewrite scalerCA scalerA mulVf // scale1r -divp_eq. suff s : size (p %% d) < size (c *: d) by rewrite (modpP e s). by rewrite size_scale ?ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)