simp [mod, div]
a b c : ℤα
h : b ≠ 0
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
a b c : ℤα
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤα (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)