proposition: Lemma ptd_f2 (f : R -> R -> R) s : sorted Rle s -> (forall x y, x <= y -> x <= f x y <= y) -> pointed_subdiv (SF_seq_f2 f s).
proof: Proof. intros Hs Hf. elim: s Hs => [ _ | h s]. intros i Hi. by apply Nat.nlt_0_r in Hi. case: s => [ | h' s] IH Hs. intros i Hi. by apply Nat.nlt_0_r in Hi. case => [ | i] Hi. apply Hf, Hs. apply IH. apply Hs. by apply Nat.succ_lt_mono. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy