proposition: Lemma SF_map_sort (f : T -> T0) (s : SF_seq) (Ord : R -> R -> Prop) : SF_sorted Ord s -> SF_sorted Ord (SF_map f s).
proof: Proof. unfold SF_sorted ; apply SF_cons_ind with (s := s) => {s} /= [x0 | [x0 _] /= s IH] Hs. by []. split. by apply Hs. now apply IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy