rw [inclusion]
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (↑inclusion { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤
    |2⁻¹|