proposition: Lemma SF_sup_fun_bound (f : R -> R) (a b : R) (n : nat) (x : R) : SF_sup_fun f a b n x = SF_sup_fun f b a n x.
proof: Proof. rewrite /SF_sup_fun ; case: (Rle_dec a b) => Hab ; case : (Rle_dec b a) => Hba //. by rewrite (Rle_antisym _ _ Hab Hba). by contradict Hba ; apply Rlt_le, Rnot_le_lt. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy