proposition: Lemma SF_cut_up_step s x eps : SF_h s <= x <= last (SF_h s) (SF_lx s) -> seq_step (SF_lx s) < eps -> seq_step (SF_lx (SF_cut_up s x)) < eps.
proof: Proof. unfold SF_cut_down, seq_step ; simpl. case => Hh Hl. case: Rle_dec => //= _. move: {4 5}(SF_h s) Hh Hl ; apply SF_cons_ind with (s := s) => {s} [ x1 | [x1 y0] s IH ] /= x0 Hh Hl He. by apply He. case: Rle_dec => //= Hx. apply (IH x0) => //=. apply Rle_lt_trans with (2 := He). by apply Rmax_r. apply Rle_lt_trans with (2 := He). apply Rnot_le_lt in Hx. apply Rmax_case. apply Rle_trans with (2 := Rmax_l _ _). rewrite ?Rabs_pos_eq. by apply Rplus_le_compat_l, Ropp_le_contravar. rewrite -Rminus_le_0 ; by apply Rlt_le, Rle_lt_trans with x. rewrite -Rminus_le_0 ; by apply Rlt_le. by apply Rmax_r. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy