fact: Definition SF_val_ly {T} (f : R -> T) (a b : R) (n : nat) : seq T := behead (pairmap (fun x y => f ((x+y)/2)) 0 (unif_part a b n)).
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy