proposition: Lemma bound_poly_accr_bound_gt0 (z : creal) (q : {poly {poly F}}) (a r : F) : 0 < bound_poly_accr_bound z q a r.
proof: Proof. rewrite (lt_le_trans _ (bound_poly_accr_boundP _ 0%N _ _ _)) //. by rewrite poly_accr_bound_gt0. 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)