no goals
𝓕 : Type ?u.97651
𝕜 : Type ?u.97654
α : Type ?u.97657
ι : Type ?u.97660
κ : Type ?u.97663
E : Type u_1
F : Type ?u.97669
G : Type ?u.97672
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖
simpa only [div_div_div_cancel_right'] using norm_sub_norm_le' (u / w) (v / w)