proposition: Lemma SF_cut_up_l s x : x <= last (SF_h s) (SF_lx s) -> last (SF_h (SF_cut_up s x)) (SF_lx (SF_cut_up s x)) = last (SF_h s) (SF_lx s).
proof: Proof. unfold SF_cut_down ; simpl. case: Rle_dec => //=. move: {3 4}(SF_h s); apply SF_cons_ind with (s := s) => {s} [x1 | [x1 y1] s IH ] /= x0 Hx Hx'. by apply Rle_antisym. case: Rle_dec => //= {} Hx. by apply IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy