proposition: Lemma max_size_evalX u : size u.['X] <= sizeY u + (size u).-1.
proof: Proof. rewrite horner_coef (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP=> i _. rewrite (leq_trans (size_mul_leq _ _)) // size_polyXn addnS. by rewrite leq_add ?max_size_coefXY //= -ltnS (leq_trans _ (leqSpred _)). 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)