proposition: Lemma lin_dc : forall k a a' b b' n, de_casteljau (fun j => (a * b j + a' * b' j)%R) k n = (a * de_casteljau b k n + a' * de_casteljau b' k n)%R.
proof: Proof. elim => [ | k IHk] a a' b b' n /= ; first by []. rewrite 2!IHk !mulrDr !mulrA !(mulrC r) !(mulrC l) !addrA. by rewrite (addrAC _ _ (a' * l * _)%R). 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