proposition: Lemma locally_2d_1d : forall (P : R -> R -> Prop) x y, locally_2d P x y -> locally_2d (fun u v => forall t, 0 <= t <= 1 -> locally_2d P (x + t * (u - x)) (y + t * (v - y))) x y.
proof: Proof. intros P x y H. apply locally_2d_1d_strong in H. apply: locally_2d_impl H. apply locally_2d_forall => u v H t Ht. specialize (H t Ht). apply locally_singleton with (1 := H). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub