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