proposition: Lemma SF_sup_r_bound (f : R -> R) (a b : R) (n : nat) : forall x, SF_sup_r f a b n x = SF_sup_r f b a n x.
proof: Proof. move => x /= ; by rewrite SF_sup_fun_bound. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy