simpa [coe_eq_zero] using h
case h
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ¬OneHom.toFun (↑↑inclusion) b = 0
no goals