proposition: Lemma close_trans (x y z : M) : close x y -> close y z -> close x z.
proof: Proof. intros H1 H2 eps. rewrite (double_var eps) -[eps / 2]/(pos (pos_div_2 eps)). now eapply ball_triangle. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub