no goals
α : Type ?u.18232
V : Type u_2
P : Type u_1
W : Type ?u.18241
Q : Type ?u.18244
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v v' : V
p p' : P
⊢ dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
simpa [(dist_vadd_cancel_right)] using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')