proposition: Lemma rmodpD p q : rmodp (p + q) d = rmodp p d + rmodp q d.
proof: Proof. rewrite [p in LHS]rdivp_eq [q in LHS]rdivp_eq addrACA -mulrDl. rewrite rmodp_addl_mul_small //; apply: (leq_ltn_trans (size_add _ _)). by rewrite gtn_max !ltn_rmodp // monic_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)