fact: Definition bound_poly_accr_bound (z : creal) (q : {poly {poly F}}) (a r : F) := maxr 1 (2%:R * r) ^+ (sizeY q).-1 * (1 + \sum_(i < (sizeY q).-1) bound_poly_bound z q a r i).
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)