proposition: Lemma locally_ex_not : forall (x : T) (P : T -> Prop), locally x (fun y => not (P y)) -> {d : posreal | forall y, ball x d y -> not (P y)}.
proof: Proof. intros x P H. apply locally_not'. destruct H as [eps He]. intros H. now apply (H eps). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub