proposition: Lemma SF_cut_up_cons_2 h ptd x : fst h <= SF_h ptd <= x -> SF_cut_up (SF_cons h ptd) x = SF_cut_up ptd x.
proof: Proof. intros [H0 Hx0]. rewrite /SF_cut_up /=. case: Rle_dec (Rle_trans _ _ _ H0 Hx0) => //= _ _. case: Rle_dec => //= _. move: {2 3}(SF_h ptd) Hx0 ; apply SF_cons_ind with (s := ptd) => {ptd H0} [ x0 | [x0 y0] ptd IH ] //= x0' Hx0. case: Rle_dec => //= Hx1. by apply IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy