proposition: Lemma dcn_deltan : forall n i A B, de_casteljau A B (delta i%nat) n i = A ^+ n.
proof: Proof. elim=> [|n ihn] i A B /=; first by rewrite /delta eqxx expr0. by rewrite !ihn dc_delta_lt ?ltnSn // mulr0 exprS addr0. 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