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