proposition: Lemma bound_poly_accr_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) : poly_accr_bound q.[(z i)%:P] a r <= bound_poly_accr_bound z q a r.
proof: Proof. rewrite /poly_accr_bound /bound_poly_accr_bound /=. set ui := _ ^+ _; set u := _ ^+ _; set vi := 1 + _. apply: le_trans (_ : u * vi <= _). rewrite ler_wpmul2r //. by rewrite addr_ge0 ?ler01 // sumr_ge0 //= => j _; rewrite poly_bound_ge0. rewrite /ui /u; case: (ltP 1%R); last by rewrite !expr1n. move=> r2_gt1; rewrite ler_eexpn2l //. rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //. by rewrite max_size_evalC. rewrite ler_wpmul2l ?exprn_ge0 ?le_maxr ?ler01 // ler_add //. pose f j := poly_bound q.[(z i)%:P]^`N(j.+1) a r. rewrite (big_ord_widen (sizeY q).-1 f); last first. rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //. by rewrite max_size_evalC. rewrite big_mkcond /= ler_sum // /f => k _. by case: ifP=> _; rewrite ?bound_poly_bound_ge0 ?bound_poly_boundP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)