proposition: Lemma prod_ball_sym : forall (x y : U * V) (eps : R), prod_ball x eps y -> prod_ball y eps x.
proof: Proof. intros x y eps [H1 H2]. split ; now apply ball_sym. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub