proposition: Lemma drop_polyMXn m n p : drop_poly m (p * 'X^n) = drop_poly (m - n) p * 'X^(n - m).
proof: Proof. have [->|p_neq0] := eqVneq p 0; first by rewrite mul0r !drop_poly0r mul0r. apply/polyP => i; rewrite !(coefMXn, coef_drop_poly) ltn_subRL [(m + i)%N]addnC. have [i_small|i_big]// := ltnP; congr nth. by have [mn|/ltnW mn] := leqP m n; rewrite (eqP mn) (addn0, subn0) (subnBA, addnBA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)