no goals
α : Type u_2
β : Type u_1
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y
simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y