proposition: Lemma dicho_r_correct (n : nat) (l : seq rat) (k : nat) : (size l <= n.+1)%nat -> (k <= n)%nat -> ratr (nth 0 (dicho_r n l) k) = dicho (R := R) (1/(1+1)) (1/(1+1)) n (fun i => ratr (nth 0 l i)) k.
proof: Proof. move => sl kn. rewrite /dicho_r /dicho. have kn' : (k < size (iota 0 n.+1))%nat. by rewrite size_iota. rewrite (nth_map 0%nat 0 (fun v => casteljau l (n - v) v)) //. by rewrite nth_iota // add0n casteljau_correct. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype order) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(mxalgebra perm zmodp matrix ssrint) mathcomp(seq rat) pol square_free casteljau desc mathcomp(ssrnum ssrint realalg poly) poly_normal