proposition: Lemma max_size_evalC u x : size u.[x%:P] <= sizeY u.
proof: Proof. rewrite horner_coef (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP=> i _. rewrite (leq_trans (size_mul_leq _ _)) // -polyC_exp size_polyC addnC -subn1. by rewrite (leq_trans _ (max_size_coefXY _ i)) // leq_subLR leq_add2r leq_b1. 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)