proposition: Lemma SF_sup_bound (f : R -> R) (a b : R) (n : nat) : SF_rev (SF_sup_seq f a b n) = SF_sup_seq f b a n.
proof: Proof. rewrite /SF_sup_seq unif_part_bound => //. rewrite SF_rev_f2 ?revK //. move => x y ; apply Sup_fct_bound. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy