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