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