proposition: Lemma SF_val_ly_bound {T} (f : R -> T) (a b : R) (n : nat) : SF_val_ly f a b n = rev (SF_val_ly f b a n).
proof: Proof. rewrite /SF_val_ly (unif_part_bound b a). case: (unif_part a b n) => [| h s] // ; elim: s h => [| h0 s IH] h //=. rewrite ?rev_cons. replace (pairmap (fun x y : R => f ((x + y) / 2)) 0 (rcons (rcons (rev s) h0) h)) with (rcons (pairmap (fun x y : R => f ((x + y) / 2)) 0 (rcons (rev s) h0)) (f ((h0+h)/2))). rewrite behead_rcons. rewrite rev_rcons Rplus_comm -rev_cons -IH //. rewrite size_pairmap size_rcons ; apply Nat.lt_0_succ. move: (0) h h0 {IH} ; apply rcons_ind with (s := s) => {s} [| s h1 IH] x0 h h0 //. rewrite ?rev_rcons /= IH //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy