proposition: Lemma take_poly_rmodp n p : take_poly n p = rmodp p 'X^n.
proof: Proof. have mX := monicXn R n; rewrite -[p in RHS](poly_take_drop n) rmodpD//. by rewrite rmodp_small ?rmodp_mull ?addr0// size_polyXn ltnS size_take_poly. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)