fact: Fixpoint horner_seqop_rec (cf : seq (int -> R)) (u : int -> R) n n0 := match cf with | [::] => 0 | [:: a] => a n0 * u n | a :: cf' => horner_seqop_rec cf' u (int.shift 1%N n) n0 + a n0 * u n end.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz