∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} [ProperSpace E],
  0 ≤ ε → 0 ≤ δ → ∀ (a b : E), Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)