proposition: Lemma dc_delta_lt : forall k A B i j, (j > i)%nat -> de_casteljau A B (delta i) k j = 0.
proof: Proof. elim=> [|k ihk] A B i j hlt /=. by move: hlt; rewrite ltn_neqAle; case/andP; move/negPf; rewrite /delta; move->. rewrite !ihk // ?mulr0 ?addr0 //; apply: ltn_trans hlt _; exact: ltnSn. 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