rw [mul_comm] at this
case mk
a b c : ℤα
x y : ℝ
this : |y - 2⁻¹ * rt7 * ↑(round ((2⁻¹ * rt7)⁻¹ * y))| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|