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