no goals
α : Type ?u.14646
V : Type u_1
P : Type u_2
W : Type ?u.14655
Q : Type ?u.14658
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
x y z : P
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z
rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]