proposition: Lemma dicho'_correct : forall (a b m : R)(alpha := (b - m) * (b - a)^-1) (beta := ((m - a) * (b - a)^-1))(p : nat)(q : {poly R})(c : nat -> R), a != b -> m != a -> q = \sum_(i < p.+1) c i *: bernp a b p i -> q = \sum_(j < p.+1) dicho' alpha beta c j *: bernp a m p j.
proof: Proof. move=> a b m alpha beta p q c neqab neqma qdef. have {neqma qdef} -> : q = \sum_(j < p.+1) \sum_(i < p.+1) (c i)%:P * (dicho' alpha beta (delta R i) j)%:P * bernp a m p j. rewrite exchange_big /= qdef; apply: congr_big; [by [] | by [] |]. case=> k hk _ /=. have hk': (k <= p)%N by exact: hk. rewrite (dicho'_delta_bern neqab neqma hk'). rewrite -mul_polyC big_distrr /=; apply: congr_big; [by [] | by [] |]. by case=> i hi _; rewrite !mulrA. apply: congr_big; [by [] | by [] |]. case=> i hi _ /=; rewrite -big_distrl /= -mul_polyC; congr (_ * _). have -> : dicho' alpha beta c i = dicho' alpha beta (fun k => \sum_(j < p.+1)(c j) * (delta R j k)) i. apply: ext_dc=> k _; rewrite add0n => h. have pk : (k < p.+1)%N by apply: leq_ltn_trans hi. rewrite (bigD1 (Ordinal pk)) //= /delta eqxx mulr1 big1 ?addr0 //. case=> j hj /=; move/negPf; case e : (j == k); last by rewrite mulr0. suff : Ordinal hj = Ordinal pk by move/eqP->. by apply: val_inj=> /=; apply/eqP. elim: p i {hi} c alpha beta=> [| p ihp] i c alpha beta /=; set f := dicho' alpha beta. rewrite big_ord_recl /= big_ord0 /dicho' /= addr0. rewrite /f /dicho'. have : forall k, (0 <= k)%N -> (k <= 0 + i)%N -> \sum_(j < 1) c j * delta R j k = (c 0%N) * (delta R 0) k. by move=> k _ _; rewrite big_ord_recl /= big_ord0 addr0. by move/ext_dc->; rewrite scal_dc polyCM. rewrite (_ : f _ _ = f (fun k : nat => (\sum_(j < p.+1) c j * delta R j k) + (c p.+1 * delta R p.+1 k)) i); last first. by apply: ext_dc=> k _; rewrite add0n=> hki; rewrite big_ord_recr. rewrite /f /dicho' add_dc polyCD -ihp // big_ord_recr /=; congr (_ + _). by rewrite scal_dc polyCM. 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