proposition: Lemma SF_cut_down_h s x : SF_h s <= x -> SF_h (SF_cut_down s x) = SF_h s.
proof: Proof. unfold SF_cut_down ; simpl. by case: Rle_dec. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy