proposition: Lemma locally_2d_and : forall (P Q : R -> R -> Prop) x y, locally_2d P x y -> locally_2d Q x y -> locally_2d (fun u v => P u v /\ Q u v) x y.
proof: Proof. intros P Q x y H. apply: locally_2d_impl. apply: locally_2d_impl H. apply locally_2d_forall. now split. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub