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