proposition: Lemma rmodp_compr p q : rmodp (p \Po (rmodp q d)) d = (rmodp (p \Po q) d).
proof: Proof. elim/poly_ind: p => [|p c IH]; first by rewrite !comp_polyC !rmod0p. rewrite !comp_polyD !comp_polyM addrC rmodpD //. rewrite mulrC -rmodp_mulmr // IH rmodp_mulmr //. rewrite !comp_polyX !comp_polyC. by rewrite mulrC rmodp_mulmr // -rmodpD // addrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)