proposition: Lemma dc_deltaS : forall k A B i j, de_casteljau A B (delta i.+1) k j.+1 = de_casteljau A B (delta i) k j.
proof: Proof. elim=> [|k ihk] A B i j /=; last by rewrite !ihk. case e : (i == j); first by rewrite /delta (eqP e) !eqxx. by rewrite /delta eqSS e. 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