proposition: Lemma AbsRing_ball_triangle : forall (x y z : K) (e1 e2 : R), AbsRing_ball x e1 y -> AbsRing_ball y e2 z -> AbsRing_ball x (e1 + e2) z.
proof: Proof. intros x y z e1 e2 H1 H2. unfold AbsRing_ball. replace (minus z x) with (plus (minus y x) (minus z y)). apply: Rle_lt_trans (abs_triangle _ _) _. now apply Rplus_lt_compat. rewrite plus_comm /minus plus_assoc. apply (f_equal (fun y => plus y _)). rewrite <- plus_assoc. now rewrite plus_opp_l plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub