proposition: Lemma SF_cut_down_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_down s x)) < eps.
proof: Proof. unfold SF_cut_down, seq_step ; simpl. case => Hh Hl. case: Rle_dec => //= _. move: Hh Hl ; apply SF_cons_ind with (s := s) => {s} [ x1 | [x1 y0] s IH ] /= Hx Hh Hl. rewrite (Rle_antisym _ _ Hx Hh) Rminus_eq_0 Rabs_R0. rewrite /Rmax ; by case: Rle_dec. case: Rle_dec => //= Hx'. apply Rmax_case. apply Rle_lt_trans with (2 := Hl) ; by apply Rmax_l. apply IH ; try assumption. apply Rle_lt_trans with (2 := Hl) ; by apply Rmax_r. apply Rle_lt_trans with (2 := Hl). apply Rmax_case ; apply Rle_trans with (2 := Rmax_l _ _). rewrite ?Rabs_pos_eq. apply Rplus_le_compat_r. by apply Rlt_le, Rnot_le_lt. rewrite -Rminus_le_0. apply Rle_trans with x. by []. by apply Rlt_le, Rnot_le_lt. by rewrite -Rminus_le_0. by apply Rabs_pos. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy