proposition: Lemma add_dc k b b' n : de_casteljau (fun j => b j + b' j)%R k n = (de_casteljau b k n + de_casteljau b' k n)%R.
proof: Proof. have := lin_dc k 1 1 b b' n. rewrite (@ext_dc k (fun j => 1 * b j + 1 * b' j) (fun j => b j + b' j))%R. by rewrite !mul1r. by move => x; rewrite /= !mul1r. 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