proposition: Lemma drop_poly_rdivp n p : drop_poly n p = rdivp p 'X^n.
proof: Proof. rewrite -[p in RHS](poly_take_drop n) addrC rdivp_addl_mul ?monicXn//. by rewrite rdivp_small ?addr0// size_polyXn ltnS size_take_poly. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)