proposition: Lemma SF_sup_lx (f : R -> R) (a b : R) (n : nat) : SF_lx (SF_sup_seq f a b n) = unif_part a b n.
proof: Proof. apply SF_lx_f2. now apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy