proposition: Lemma locally_2d_ex_dec : forall P x y, (forall x y, P x y \/ ~P x y) -> locally_2d P x y -> {d : posreal | forall u v, Rabs (u-x) < d -> Rabs (v-y) < d -> P u v}.
proof: Proof. intros P x y P_dec H. destruct (locally_ex_dec (x, y) (fun z => P (fst z) (snd z))) as [d Hd]. - now intros [u v]. - destruct H as [e H]. exists e. intros [u v] Huv. apply H. apply Huv. apply Huv. exists d. intros u v Hu Hv. apply (Hd (u, v)). simpl. now split. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub