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 != b -> q = \sum_(i < p.+1) c i *: bernp a b p i -> q = \sum_(j < p.+1) dicho alpha beta p c j *: bernp m b p j.
proof: Proof. move=> a b m alpha beta p q c neqab neqmb qdef. rewrite bern_rev_coef in qdef. have neqba : b != a by rewrite eq_sym. rewrite (@dicho'_correct _ _ _ _ _ (fun i => c (p - i)%N) neqba neqmb qdef). rewrite -(big_mkord (fun _ => true) (fun j => dicho' ((a - m) / (a - b)) ((m - b) / (a - b)) (fun i : nat => c (p - i)%N) j *: bernp b m p j)). rewrite big_nat_rev /= big_mkord; apply: congr_big; [by [] | by [] |]. move=> [i hi] _ {qdef}; rewrite add0n subSS. rewrite -bern_swap //; congr (_ *: _); rewrite /dicho' /dicho. rewrite dc_reverse //= ?leq_subr // addn0 subKn //. rewrite -opprB -[a - b]opprB -[a - m]opprB -mulN1r -[-(b - a)]mulN1r. rewrite -[-(m - a)]mulN1r invfM [(- 1)^-1]invrN invr1 -mulrA. rewrite [(b - m) * _]mulrC !mulrA mulNr mul1r opprK [-1 * _ ]mulrC 2!mulrN1. by rewrite opprK -/beta mulrC 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