proposition: Lemma ball_norm_dec : forall (x y : V) (eps : posreal), {ball_norm x eps y} + {~ ball_norm x eps y}.
proof: Proof. intros x y eps. apply Rlt_dec. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub