proposition: Lemma drop_poly_eq0 m p : size p <= m -> drop_poly m p = 0.
proof: Proof. move=> sLm; apply/polyP => i; rewrite coef_poly coef0 ltn_subRL addnC. by rewrite if_nth ?leqVgt// nth_default// (leq_trans _ (leq_addl _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)