proposition: Lemma locally_2d_impl_strong : forall (P Q : R -> R -> Prop) x y, locally_2d (fun u v => locally_2d 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 Li LP. apply locally_2d_locally in Li. apply locally_2d_locally in LP. apply locally_locally in LP. apply locally_2d_locally. generalize (filter_and _ _ Li LP). apply filter_imp. intros [u v] [H1 H2]. apply H1. now apply locally_2d_locally. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub