proposition: Lemma bernp_first_coeff0 l d (a b : R) q : a != b -> (0 < d)%N -> q = \sum_(i < d.+1) l`_i *: bernp a b d i -> (l`_0 == 0) = (q.[a] == 0).
proof: Proof. move=> anb dn0 qq. rewrite qq horner_sum big_ord_recl !hornerE. rewrite (_ : \sum_(i < d) _ = 0). by rewrite addr0 mulf_eq0 bern0_a // eqxx orbF. apply: big1; move=> [i ci] _ /=; apply/eqP. by rewrite hornerE mulf_eq0 bern0_a // [bump _ _ == _]eq_sym neq_bump orbT. 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