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