proposition: Lemma dc_delta_tail : forall i k A B, de_casteljau A B (delta i) (i + k)%nat 0 = A ^+ k * B ^+ i *+'C(k + i, i).
proof: Proof. elim=> [|i ihi] k A B /=; rewrite -?addnE. by rewrite add0n addn0 /= expr0 mulr1 bin0 dcn_deltan mulr1n. rewrite dc_deltaS ihi. elim: k => [|k ihk] /=. rewrite !add0n !expr0 !addn0 !mul1r dc_delta_gt ?mulr0 ?add0r 1?mulrC ?subSnn //. by rewrite !binn !mulr1n exprS mulrC. rewrite !addnS /= dc_deltaS ihi ihk !addnS !addSn !mulrnAr mulrA -exprS. rewrite [_ * B^+ i]mulrC mulrA -exprS [B^+_ * _]mulrC -mulrnDr. by congr (_ *+ _). 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