proposition: Lemma closed_le : forall y : R, closed (fun u : R => u <= y).
proof: Proof. intros y. apply closed_ext with (fun u => not (Rlt y u)). intros x. split. apply Rnot_lt_le. apply Rle_not_lt. apply closed_not. apply open_gt. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub