proposition: Lemma take_polyMXn m n p : take_poly m (p * 'X^n) = take_poly (m - n) p * 'X^n.
proof: Proof. have [->|/eqP p_neq0] := p =P 0; first by rewrite !(mul0r, take_poly0r). apply/polyP => i; rewrite !(coef_take_poly, coefMXn). by have [iLn|nLi] := leqP n i; rewrite ?if_same// ltn_sub2rE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)