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