proposition: Lemma bern0_a : forall (a b : R) deg i, a != b -> (0 < deg)%N -> (i <= deg)%N -> (bernp a b deg i).[a] == 0 = (i != 0)%N.
proof: Proof. move=> a b deg i anb dn0 id. rewrite /bernp hornerMn !hornerE subrr. rewrite mulrn_eq0 !mulf_eq0 !expf_eq0 eqxx andbT invr_eq0 expf_eq0 dn0 andTb. rewrite subr_eq0 [b == a]eq_sym (negbTE anb) orFb lt0n andbF orbF. by rewrite eqn0Ngt bin_gt0 id. 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