𝓕 : Type ?u.69547
𝕜 : Type ?u.69550
α : Type ?u.69553
ι : Type ?u.69556
κ : Type ?u.69559
E : Type u_1
F : Type ?u.69565
G : Type ?u.69568
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ 0 ≤ dist a 1
𝓕 : Type ?u.69547
𝕜 : Type ?u.69550
α : Type ?u.69553
ι : Type ?u.69556
κ : Type ?u.69559
E : Type u_1
F : Type ?u.69565
G : Type ?u.69568
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ 0 ≤ ‖a‖
rw [← dist_one_right]
no goals
𝓕 : Type ?u.69547
𝕜 : Type ?u.69550
α : Type ?u.69553
ι : Type ?u.69556
κ : Type ?u.69559
E : Type u_1
F : Type ?u.69565
G : Type ?u.69568
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ 0 ≤ dist a 1
exact dist_nonneg