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