proposition: Lemma max_size_coefXY u i : size u`_i <= sizeY u.
proof: Proof. have [ltiu | /(nth_default 0)->] := ltnP i (size u); last by rewrite size_poly0. exact: (bigmax_sup (Ordinal ltiu)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)