proposition: Lemma coef_drop_poly m p i : (drop_poly m p)`_i = p`_(i + m).
proof: Proof. by rewrite coef_poly ltn_subRL addnC if_nth ?leqVgt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)