fact: Fixpoint casteljau (l : seq rat) (n : nat) : nat -> rat := match n with O => fun j => nth 0 l j | S p => fun j => ((casteljau l p j + casteljau l p j.+1)/(1+1))%R end.
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