proposition: Lemma fct_ball_triangle (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. by move=> xy yz t; apply: (@ball_triangle _ _ (y t)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed