proposition: Lemma locally_2d_singleton : forall (P : R -> R -> Prop) x y, locally_2d P x y -> P x y.
proof: Proof. intros P x y LP. apply locally_2d_locally in LP. apply locally_singleton with (1 := LP). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub