proposition: Lemma locally_interval (P : R -> Prop) (x : R) (a b : Rbar) : Rbar_lt a x -> Rbar_lt x b -> (forall (y : R), Rbar_lt a y -> Rbar_lt y b -> P y) -> locally x P.
proof: Proof. move => Hax Hxb Hp. case: (Rbar_lt_locally _ _ _ Hax Hxb) => d Hd. exists d => y Hy. now apply Hp ; apply Hd. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub