proposition: Lemma SF_cut_down_pointed s x : SF_h s <= x -> pointed_subdiv s -> pointed_subdiv (SF_cut_down s x).
proof: Proof. unfold SF_cut_down ; simpl. case: Rle_dec => //= _. apply SF_cons_ind with (s := s) => {s} [x0 | [x1 y1] s IH] /= Hx0 H. move => i /= Hi. unfold SF_size in Hi ; simpl in Hi. apply Nat.lt_succ_r, Nat.le_0_r in Hi. rewrite Hi ; simpl ; split. by []. by apply Rle_refl. case: Rle_dec => //= Hx1. move: (H O (Nat.lt_0_succ _)) => /= H0. apply ptd_cons in H. move: (IH Hx1 H) => {} IH. rewrite /pointed_subdiv => i. destruct i => /= Hi. by apply H0. apply (IH i). apply Nat.succ_lt_mono, Hi. move => i /= Hi. unfold SF_size in Hi ; simpl in Hi. apply Nat.lt_succ_r, Nat.le_0_r in Hi. rewrite Hi ; simpl ; split. apply Rmin_case. apply (H O). by apply Nat.lt_0_succ. by []. by apply Rmin_r. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy