proposition: Lemma locally_2d_align : forall (P Q : R -> R -> Prop) x y, ( forall eps : posreal, (forall u v, Rabs (u - x) < eps -> Rabs (v - y) < eps -> P u v) -> forall u v, Rabs (u - x) < eps -> Rabs (v - y) < eps -> Q u v ) -> locally_2d P x y -> locally_2d Q x y.
proof: Proof. intros P Q x y K (d,H). exists d => u v Hu Hv. now apply (K d). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub