proposition: Lemma drop_polyMXn_id n p : drop_poly n (p * 'X^ n) = p.
proof: Proof. by rewrite drop_polyMXn subnn drop_poly0l expr0 mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)