proposition: Lemma leq_sizeP p i : reflect (forall j, i <= j -> p`_j = 0) (size p <= i).
proof: Proof. apply: (iffP idP) => [hp j hij| hp]. by apply: nth_default; apply: leq_trans hij. case: (eqVneq p) (lead_coef_eq0 p) => [->|p0]; first by rewrite size_poly0. rewrite leqNgt; apply/contraFN => hs. by apply/eqP/hp; rewrite -ltnS (ltn_predK hs). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)