proposition: Lemma locally_locally : forall (x : T) (P : T -> Prop), locally x P -> locally x (fun y => locally y P).
proof: Proof. intros x P [dp Hp]. exists (pos_div_2 dp). intros y Hy. exists (pos_div_2 dp) => /= z Hz. apply Hp. rewrite (double_var dp). now apply ball_triangle with y. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub