proposition: Lemma dicho'_delta_bern (a b m : R) k p (alpha := (b - m) * (b - a)^-1) (beta := ((m - a) * (b - a)^-1)) : a != b -> m != a -> (k <= p)%N -> bernp a b p k = \sum_(j < p.+1)((dicho' alpha beta (delta R k) j)%:P * bernp a m p j).
proof: Proof. move=> dab dma hlt1. rewrite -(big_mkord (fun _ => true) (fun j => (dicho' alpha beta (delta R k) j)%:P * bernp a m p j)). rewrite (big_cat_nat _ _ _ (leq0n k)) //=; last by apply: leq_trans hlt1 _; exact: leqnSn. rewrite (_ : \sum_( _ <= i0 < _ ) _ = 0) /= ?add0r; last first. rewrite big1_seq //= => j; rewrite mem_iota add0n subn0; case/andP=> _ h. by rewrite dc_delta_head // polyC0 mul0r. rewrite -{2}(add0n k) big_addn. have h : forall i0, (0 <= i0 < p - k)%nat -> (dicho' (m - a) (b - m) (delta R k) (i0 + k))%:P * bernp a m p (i0 + k) = (( (m - a) ^+ i0) * (b - m) ^+ k)%:P * bernp a m p (i0 + k) *+ 'C(i0 + k, k). by move=> j h; rewrite /dicho' addnC dc_delta_tail polyCMn -mulrnAl addnC. have -> : bernp a b p k = (('X - a%:P)^+k * ((b - a)^-k)%:P) * ((b%:P - 'X )^+(p - k) * ((b - a)^-(p - k))%:P) *+'C(p, k). rewrite /bernp -!mulrA. congr (_ *+ _). rewrite [_ * (_)%:P]mulrC [((b - a)^-k)%:P * _]mulrA -polyCM. by rewrite -invfM -exprD subnKC // !mulrA [_ %:P * _]mulrC. have -> : (('X - a%:P) ^+ k * ((b - a) ^- k)%:P) = (beta^+k)%:P * (('X - a%:P) ^+ k * ((m - a) ^- k)%:P). rewrite /beta expr_div_n polyCM !mulrA -[_ * (_ ^+k)]mulrC !mulrA mulrAC. rewrite -!mulrA -polyCM mulfV ?polyC1 ?mulr1 ?expf_eq0 ?subr_eq0 //. by move/negPf: dma => ->; rewrite andbF. rewrite -(exprVn (b - a)) [(_ ^-1 ^+ _)%:P]polyC_exp. rewrite -exprMn_comm; last by exact: mulrC. have -> : (b%:P - 'X) * ((b - a)^-1)%:P = ((m%:P - 'X) * (m - a)^-1%:P) + (alpha%:P * ('X - a%:P) * (m - a)^-1%:P). rewrite [(m%:P - _) * _]mulrDl mulrDr [(alpha%:P * _ + _) * _]mulrDl. rewrite (mulrC _ 'X) -(mulrA 'X) [_ + (- 'X * _)]addrC mulNr -mulrN. rewrite addrAC addrA -mulrDr -mulN1r -mulrDl. rewrite -(polyCN 1) -polyCD /alpha. have -> : -1 = (a-b)/(b-a). by rewrite -opprB mulNr mulfV // subr_eq0 eq_sym. rewrite -mulrDl addrA addrNK -(opprB m a). rewrite -polyCM !mulNr mulrAC mulfV ?mul1r; last by rewrite subr_eq0. rewrite polyCN -addrA -mulrDl [_ * - a%:P]mulrC -[-a%:P]polyCN. rewrite -polyCM -polyCD !mulrA. have {2}-> : m = m * (b - a) / (b - a) by rewrite mulfK // subr_eq0 eq_sym. rewrite -[_ + _ /(b-a)]mulrDl !mulrDr addrA addrAC [-a * -m]mulrN. rewrite [-a * m]mulrC addrNK [_ + m * b]addrC -mulrDl -polyCM. rewrite [_ * b]mulrC mulrAC mulfK; last by rewrite subr_eq0. by rewrite mulrN -mulNr polyCM -mulrDl addrC. rewrite [_^+ (p - k)]exprDn /= subSn //. rewrite -(big_mkord (fun _ => true) (fun i => ((m%:P - 'X) * ((m - a)^-1)%:P) ^+ (p - k - i) * (alpha%:P * ('X - a%:P) * ((m - a)^-1)%:P) ^+ i *+ 'C( p - k, i))). rewrite big_distrr /= (big_morph _ (mulrnDl ('C(p, k))) (mul0rn _ _)). apply: congr_big_nat=> // i /= hi. rewrite /dicho' [(i + k)%nat]addnC dc_delta_tail /bernp. rewrite !mulrnAr polyCMn mulrnAl -!mulrnA; congr (_ *+ _); last first. rewrite addnC -util_C ?leq_addr //. by rewrite mulnC; congr (_ * _)%N; rewrite addnC addnK. by move:hi; rewrite ltnS -(leq_add2l k) subnKC. set Xa := ('X - a%:P); set Xb := (_ - 'X). rewrite [alpha^+_ * _]mulrC [(beta^+_ * _)%:P]polyCM -!mulrA; congr (_ * _). rewrite [(alpha%:P * _)]mulrC. rewrite [(_ * alpha%:P)^+i]exprMn_comm; last by exact: mulrC. set lhs := (alpha ^+ i)%:P * _; rewrite !mulrA. rewrite [_ * alpha%:P ^+ i]mulrC /lhs polyC_exp; congr (_ * _)=> {lhs alpha}. set lhs := _ * (_ * Xb ^+ (p - _)). rewrite !exprMn_comm; try exact: mulrC. rewrite [Xa^+i * _]mulrC !mulrA [_ * Xa^+ _]mulrC !mulrA. rewrite -exprD /lhs [_ * (Xa^+ _ * _)]mulrA [_ * Xa^+ _]mulrC -!mulrA. rewrite addnC; congr (_ * _)=> {lhs}. rewrite !mulrA [_ * Xb^+ (p - k - i)]mulrC -!mulrA [Xb^+ _ * _]mulrC. rewrite subnDA; congr (_ * _); rewrite -!polyC_exp -!polyCM; congr (_ %:P). rewrite -!exprVn -!exprD; congr ((m -a)^-1 ^+ _). rewrite subnK; last by []. by rewrite addnC subnK; last by []. 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