fact: Definition poly_accr_bound (p : {poly F}) (a r : F) : F := (maxr 1 (2%:R * r)) ^+ (size p).-1 * (1 + \sum_(i < (size p).-1) poly_bound p^`N(i.+1) a r).
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)