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