proposition: Lemma scal_dc k a b n : de_casteljau (fun j => a * b j)%R k n = (a * de_casteljau b k n)%R.
proof: Proof. have := lin_dc k a 0 b (fun i => 0)%R n. rewrite (@ext_dc _ (fun j => a * b j + 0 * 0)%R (fun j => a * b j)%R). by rewrite mul0r addr0. by move => x; rewrite /= mul0r addr0. 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