proposition: Lemma ball_norm_triangle (x y z : V) (e1 e2 : R) : ball_norm x e1 y -> ball_norm y e2 z -> ball_norm x (e1 + e2) z.
proof: Proof. intros H1 H2. eapply Rle_lt_trans, Rplus_lt_compat. 2: by apply H1. 2: by apply H2. rewrite Rplus_comm. eapply Rle_trans, norm_triangle. apply Req_le, f_equal. rewrite /minus -!plus_assoc. apply f_equal. by rewrite plus_assoc plus_opp_l plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub