norm_num
case mk
a b c : ℤα
x y : ℝ
⊢ |y - (↑(round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y)))) + ↑(round (2 * rt7⁻¹ * y)) * { re := 1 / 2, im := rt7 / 2 }).im| ≤
    |4⁻¹ * rt7|
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |1 / 4 * rt7|