proposition: Lemma ereal_ball_triangle x y z r1 r2 : ereal_ball x r1 y -> ereal_ball y r2 z -> ereal_ball x (r1 + r2) z.
proof: Proof. rewrite /ereal_ball => h1 h2; rewrite -[X in (X - _)%R](subrK (contract y)). by rewrite -addrA (le_lt_trans (ler_normD _ _)) // ltrD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed