proposition: Lemma SF_cut_up_cons_1 h ptd x : fst h <= x < SF_h ptd -> SF_cut_up (SF_cons h ptd) x = SF_cons (x,Rmax (snd h) x) ptd.
proof: Proof. intros [H0 Hx0]. apply Rlt_not_le in Hx0. rewrite /SF_cut_up /=. case: Rle_dec => //= _. by case: Rle_dec. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy