proposition: Lemma SF_sorted_f1 {T : Type} (f1 : R -> T) P Ord : (sorted Ord P) <-> (SF_sorted Ord (SF_seq_f1 f1 P)).
proof: Proof. case: P => [ | h P] //. rewrite /SF_sorted SF_lx_f1 //. by apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy