proposition: Lemma locally_2d_locally : forall P x y, locally_2d P x y <-> locally (x,y) (fun z => P (fst z) (snd z)).
proof: Proof. intros P x y. split ; intros [d H] ; exists d. - simpl. intros [u v] H'. now apply H ; apply H'. - intros u v Hu Hv. apply (H (u,v)). by split. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub