no goals
α : Type u_2
β : Type u_1
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
simpa [smul_zero] using dist_smul_pair r 0 x