proposition: Lemma ext_dc : forall k b b' n, (forall i, (n <= i)%nat -> (i <= n + k)%nat -> b i = b' i) -> de_casteljau b k n = de_casteljau b' k n.
proof: Proof. move => k b b'; elim: k => [ n q | k IHk n q] /=. by apply: q; rewrite ?addn0 leqnn. rewrite !IHk //; move => i ni nik; apply: q => //; first exact: ltnW. by move: nik; rewrite addnS addSn. by apply: leq_trans nik _; rewrite addnS leqnSn. 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