proposition: Lemma rmodpZ a p : rmodp (a *: p) d = a *: (rmodp p d).
proof: Proof. case: (altP (a =P 0%R)) => [-> | cn0]; first by rewrite !scale0r rmod0p. have -> : ((a *: p) = (a *: (rdivp p d)) * d + a *: (rmodp p d))%R. by rewrite -scalerAl -scalerDr -rdivp_eq. rewrite rmodp_addl_mul_small //. rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. rewrite size_polyC cn0 addSn add0n /= ltn_rmodp. by apply: monic_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)