proposition: Lemma SF_cut_down_cons_2 h ptd x : fst h <= SF_h ptd <= x -> SF_cut_down (SF_cons h ptd) x = SF_cons h (SF_cut_down ptd x).
proof: Proof. intros [H0 Hx0]. rewrite /SF_cut_down /=. case: Rle_dec (Rle_trans _ _ _ H0 Hx0) => //= _ _. by case: Rle_dec. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy