proposition: Lemma SF_map_lx (f : T -> T0) (s : SF_seq) : SF_lx (SF_map f s) = SF_lx s.
proof: Proof. apply SF_cons_ind with (s := s) => {s} //= h s IH ; by rewrite SF_map_cons ?SF_lx_cons IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy