proposition: Lemma open_Rbar_lt' : forall x y, Rbar_lt x y -> Rbar_locally x (fun u => Rbar_lt u y).
proof: Proof. intros [x| |] y Hxy. - now apply open_Rbar_lt. - easy. - destruct y as [y| |]. now exists y. now apply filter_forall. easy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub