proposition: Lemma casteljau_correct (l : seq rat) k n : ratr (casteljau l k n) = de_casteljau (R:=R) (1/(1+1)) (1/(1+1)) (fun i => ratr (nth 0 l i)) k n.
proof: Proof. elim : k n => [ n | k Ik n]; first by []. rewrite /= rmorphM rmorphD rmorphV; last by rewrite unitf_gt0 //. by rewrite /= rmorphD !rmorph1 !Ik mulrDl !mul1r !(mulrC (_ ^-1)). 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