proposition: Lemma poly_accr_bound2_gt0 p a r : 0 < poly_accr_bound2 p a r.
proof: Proof. rewrite /poly_accr_bound pmulr_rgt0 //. rewrite ltr_paddr ?ltr01 //. by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0. by rewrite exprn_gt0 // lt_maxr ltr01 pmulr_rgt0 ?ltr0n. 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)