proposition: Lemma bern_coeffs_mon : forall i, (i <= deg)%N -> relocate 'X^i = ((b - a)^+deg * 'C(deg, i)%:R^-1)%:P * bernp a b deg (deg - i)%N.
proof: Proof. have nsba0 : ~~ (b - a == 0) by rewrite subr_eq0 eq_sym. move=> i leqip. rewrite /bernp polyCM mulrAC -mulr_natr !mulrA -polyCM mulfV; last first. by rewrite expf_eq0 (negbTE nsba0) andbF. rewrite mul1r -!mulrA -polyCMn -polyCM bin_sub // mulfV; last first. by rewrite pnatr_eq0 -lt0n bin_gt0. rewrite subKn // mulr1. rewrite /relocate /recip size_polyXn ltnNge ltnS leqip /= shift_polyXn. have -> // : forall c : R, c != 0 -> (('X + (-1)%:P)^+ i) \scale c = ('X * c%:P + (-1)%:P)^+ i. move=> c hc; rewrite scaleX_polyE size_factor_expr. rewrite [(_ * _ + _) ^+ _]exprDn. rewrite (reindex_inj rev_ord_inj) /=. rewrite power_monom poly_def; apply: eq_bigr => j _. rewrite coef_poly subSS; have -> : (j < i.+1)%N by case j. rewrite subKn; last by case j. rewrite exprMn_comm; last by exact: mulrC. rewrite -mulrA (mulrCA 'X^j) (mulrC 'X^j) -!polyC_exp !mul_polyC. by rewrite scalerA !scalerMnl -(mulrC (c ^+ j)) mulrnAr bin_sub //; case j. have -> // : forall c:R, c != 0 -> reciprocal_pol (('X * c%:P + (-1)%:P) ^+ i) = (c%:P - 'X)^+i. move=> c hc; rewrite reciprocalX reciprocal_monom // addrC. by congr ((_ + _) ^+ _); rewrite mulrC mul_polyC scaleNr scale1r. rewrite size_amul_expr // subSS /shift_poly comp_polyM !poly_comp_exp. rewrite comp_polyD linearN /= !comp_polyX comp_polyC opprD -!polyCN opprK. by rewrite polyCB addrAC !addrA addrK. 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