ring_nf
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
⊢ 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
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 + rt3 ^ 2 * (↑(ofNat 1) / ↑16) < 1