proposition: Lemma bern_swap p i (l r : R) : (i <= p)%N -> bernp r l p i = bernp l r p (p - i).
proof: Proof. move=> lip; rewrite /bernp subKn // bin_sub //; congr (_ *+ _). rewrite -[l - r]opprB -[l%:P - 'X]opprB -['X - r%:P]opprB. rewrite -mulN1r -[-(r%:P - 'X)]mulN1r -[- ('X - l%:P)]mulN1r. rewrite !exprMn_comm; try exact: mulrC. rewrite invfM polyCM [_ * ((r - l)^-p)%:P]mulrC. rewrite -!mulrA; congr (_ * _). rewrite -exprVn polyC_exp [(- 1)^-1]invrN invr1 polyCN. rewrite [(r%:P - 'X)^+i * _]mulrC !mulrA polyC1 -!exprD. by rewrite -addnA subnKC // -signr_odd oddD addbb /= expr0 mul1r. 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