K : Type u_1
E : Type ?u.6892273
inst✝ : IsROrC K
z : K
⊢ abs (↑re z) / ‖z‖ ≤ 1
K : Type u_1
E : Type ?u.6892273
inst✝ : IsROrC K
z : K
⊢ abs (↑re z / ‖z‖) ≤ 1
rw [abs_div, abs_norm]
no goals
K : Type u_1
E : Type ?u.6892273
inst✝ : IsROrC K
z : K
⊢ abs (↑re z) / ‖z‖ ≤ 1
exact div_le_one_of_le (abs_re_le_norm _) (norm_nonneg _)