proposition: Lemma locally_2d_forall : forall (P : R -> R -> Prop) x y, (forall u v, P u v) -> locally_2d P x y.
proof: Proof. intros P x y Hp. now exists (mkposreal _ Rlt_0_1) => u v _ _. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub