proposition: Lemma SF_map_rev (f : T -> T0) s : SF_rev (SF_map f s) = SF_map f (SF_rev s).
proof: Proof. apply SF_lx_ly_inj. by rewrite SF_lx_rev ?SF_map_lx ?SF_lx_rev. by rewrite SF_ly_rev ?SF_map_ly ?SF_ly_rev map_rev. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy