proposition: Lemma SF_cut_up_pointed s x : SF_h s <= x -> pointed_subdiv s -> pointed_subdiv (SF_cut_up s x).
proof: Proof. unfold SF_cut_up ; simpl. case: Rle_dec => //= _. move: {2 3}(SF_h s) ; apply SF_cons_ind with (s := s) => {s} [ x1 | [x1 y0] s IH] /= x0 Hx0 H i Hi. by apply Nat.nlt_0_r in Hi. destruct (Rle_dec (SF_h s) x) as [Hx1|Hx1]. apply IH => //=. move: H ; by apply ptd_cons. destruct i ; simpl. split. by apply Rmax_r. apply Rmax_case. by apply (H O), Nat.lt_0_succ. by apply Rlt_le, Rnot_le_lt. apply (H (S i)), Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy