proposition: Lemma size_bernp (neqab : a != b) (i : nat) : (i <= deg)%N -> size (bernp i) = deg.+1.
proof: Proof. move=> id; rewrite /bernp. rewrite -!mulrnAl -polyCMn -mulrA. rewrite size_Cmul. rewrite size_monicM. rewrite size_exp_XsubC. have <- : (-1)%:P * ('X - b%:P) = (b%:P - 'X). by rewrite mulrBr polyCN !mulNr -polyCM mul1r opprK addrC mul1r. rewrite exprMn_comm; last by apply: mulrC. rewrite -polyC_exp size_Cmul; last first. rewrite exprnP; apply: expfz_neq0. by rewrite oppr_eq0 oner_neq0. by rewrite size_exp_XsubC addSn /= addnS subnKC. by apply/monic_exp/monicXsubC. rewrite exprnP expfz_neq0 // -size_poly_eq0. have -> : b%:P - 'X = (-1)%:P * 'X + b%:P. by rewrite addrC polyCN mulNr mul1r. rewrite size_MXaddC size_polyC. by rewrite polyCN oppr_eq0 (negbTE (oner_neq0 _)) andFb. rewrite mulrn_eq0 negb_or. rewrite invr_neq0 ?andbT; first by rewrite -lt0n bin_gt0. by rewrite expf_neq0 // subr_eq0 eq_sym. 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