proposition: Lemma Mobius_bernp i : (i <= deg)%N -> Mobius deg a b (bernp a b deg i) = ('C(deg, i))%:R *: 'X ^+ (deg - i).
proof: Proof. move=> ci; set u := _%:R; rewrite -(mul1r (bernp a b deg i)) -[1]/(1%:P). have t : (b - a)^+deg/('C(deg, i))%:R != 0. apply: mulf_neq0; first by rewrite expf_neq0 // subr_eq0 eq_sym. by rewrite invr_neq0 // pnatr_eq0 -lt0n bin_gt0. rewrite -(mulVf t) {t} polyCM -mulrA. rewrite -bin_sub // -[X in bernp a b deg X](subKn ci) -bern_coeffs_mon; last first. by rewrite leq_subr. rewrite mul_polyC MobiusZ. rewrite MobiusK; last first. by rewrite size_polyXn ltnS leq_subr. rewrite invfM scalerA mulrAC mulVf; last first. by rewrite expf_neq0 // subr_eq0 eq_sym. by rewrite mul1r invrK bin_sub. rewrite /relocate. rewrite ltnNge size_polyXn (leq_ltn_trans _ (ltnSn _)) ?leq_subr //=. rewrite size_comp_poly2; last by rewrite size_XaddC. rewrite size_recip // !size_comp_poly2 //. by rewrite size_polyXn (leq_ltn_trans _ (ltnSn _)) // leq_subr. by rewrite size_XaddC. by rewrite size_XmulC // 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