no goals
𝓕 : Type ?u.640919
𝕜 : Type ?u.640922
α : Type ?u.640925
ι : Type ?u.640928
κ : Type ?u.640931
E : Type u_1
F : Type ?u.640937
G : Type ?u.640940
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
a b : E
⊢ dist (a / b) a = ‖b‖
rw [dist_comm, dist_self_div_right]