no goals
𝓕 : Type ?u.1113180
𝕜 : Type ?u.1113183
α : Type ?u.1113186
ι : Type ?u.1113189
κ : Type ?u.1113192
E : Type ?u.1113195
F : Type ?u.1113198
G : Type ?u.1113201
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
z : ℤ
c : ℝ≥0
⊢ abs z ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c
rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.coe_natAbs z]