proposition: Lemma locally_2d_impl : forall (P Q : R -> R -> Prop) x y, locally_2d (fun u v => P u v -> Q u v) x y -> locally_2d P x y -> locally_2d Q x y.
proof: Proof. intros P Q x y (d,H). apply locally_2d_impl_strong. exists d => u v Hu Hv Hp. apply H => //. now apply locally_2d_singleton. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub