proposition: Lemma SF_size_map (f : T -> T0) s : SF_size (SF_map f s) = SF_size s.
proof: Proof. by rewrite -!SF_size_ly SF_map_ly size_map. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy