proposition: Lemma take_poly_modp n p : take_poly n p = p %% 'X^n.
proof: Proof. by rewrite RingMonic.take_poly_rmodp modpE // monicXn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)