have : |(1 / 2 : ℝ)| = 1 / 2 := by norm_num
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|
case mk
a b c : ℤα
x y : ℝ
this : |1 / 2| = 1 / 2
⊢ |x -
        (toℂ
            { z := round (x + ↑(round (rt7⁻¹ * y * 2)) * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)),
              w := round (rt7⁻¹ * y * 2) }).re| ≤
    |↑(ofNat 1) / ↑2|