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