proposition: Lemma fct_ball_triangle : forall (x y z : T -> U) (e1 e2 : R), fct_ball x e1 y -> fct_ball y e2 z -> fct_ball x (e1 + e2) z.
proof: Proof. intros x y z e1 e2 H1 H2 t. now apply ball_triangle with (y t). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub