proposition: Lemma rmodpN p : rmodp (- p) d = - (rmodp p d).
proof: Proof. rewrite {1}(rdivp_eq p) opprD // -mulNr rmodp_addl_mul_small //. by rewrite size_opp ltn_rmodp // monic_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)