proposition: Lemma rmodp_id (p : {poly R}) : rmodp (rmodp p d) d = rmodp p d.
proof: Proof. by rewrite rmodp_small // ltn_rmodpN0 // monic_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)