proposition: Lemma locally_2d_1d_const_y : forall (P : R -> R -> Prop) x y, locally_2d P x y -> locally x (fun t => P t y).
proof: Proof. intros P x y (d,Hd). exists d; intros z Hz. apply Hd. exact Hz. rewrite Rminus_eq_0 Rabs_R0; apply cond_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub