proposition: Lemma rdivpDl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d.
proof: Proof. case: (monic_comreg mond)=> Hc Hr; rewrite [r in q + r]rdivp_eq addrA. rewrite [q in q + _ + _]rdivp_eq; move/rmodp_eq0P->. by rewrite addr0 -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)