proposition: Lemma open_Rbar_gt : forall y, open (fun u : R => Rbar_lt y u).
proof: Proof. intros [y| |]. - apply open_gt. - apply open_false. - apply open_true. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub