proposition: Lemma bernp_gt0 i x : (i <= deg)%N -> a < x < b -> 0 < (bernp i).[x].
proof: Proof. move=> id /andP [ax xb]; rewrite /bernp hornerMn pmulrn_lgt0; last first. by rewrite bin_gt0. rewrite !hornerE. apply mulr_gt0; first apply mulr_gt0. by rewrite invr_gt0 exprn_gt0 // subr_gt0 (lt_trans ax). by rewrite exprn_gt0 // subr_gt0. by rewrite exprn_gt0 // subr_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc