proposition: Lemma locally_ex_dec : forall (x : T) (P : T -> Prop), (forall x, P x \/ ~P x) -> locally x P -> {d : posreal | forall y, ball x d y -> P y}.
proof: Proof. intros x P P_dec H. destruct (locally_ex_not x (fun y => not (P y))) as [d Hd]. apply: filter_imp H. intros y Py HP. now apply HP. exists d. intros y Hy. destruct (P_dec y) as [HP|HP]. exact HP. exfalso. now apply (Hd y). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub