JNBall fivefold subset six Ball

lemma JNBall.fivefold_subset_sixBall {x₀ : E} {R : ℝ} (b : JNBall x₀ R) :    Metric.ball b.center (5 * b.radius) ⊆ Metric.ball x₀ (6 * R) := by  intro y hy  have h1 : dist y b.center < 5 * b.radius := Metric.mem_ball.1 hy  have hcR : dist b.center x₀ < R := Metric.mem_ball.1 b.center_mem  have hdy : dist y x₀ < 5 * b.radius + R :=    calc dist y x₀ ≤ dist y b.center + dist b.center x₀ := dist_triangle _ _ _      _ < 5 * b.radius + R := by linarith  have h6 : 5 * b.radius + R ≤ 6 * R := by linarith [b.radius_le]  exact Metric.mem_ball.2 (lt_of_lt_of_le hdy h6)