ring_nf
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (toℂ { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (toℂ
            { z := round (x + ↑(round (rt7⁻¹ * y * 2)) * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)),
              w := round (rt7⁻¹ * y * 2) }).re| ≤
    |↑(ofNat 1) / ↑2|