norm_num
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑(ofNat 1) / ↑4 + 3 * (↑(ofNat 1) / ↑16) < 1
no goals