proposition: Lemma modpZr c p : c \in GRing.unit -> 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 mulVr // scale1r -(divp_eq ulcd). suff s : size (p %% d) < size (c *: d). by rewrite (modpP _ e s) // -mul_polyC lead_coefM lead_coefC unitrM cn0. by rewrite size_scale ?ltn_modp //; apply: contraTneq cn0 => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)