simp only [natNorm_coe] at this
a b c : ℤα
h : b ≠ 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (mod a b) < natNorm b
a b c : ℤα
h : b ≠ 0
this : ↑(natNorm (mod a b)) < ↑(natNorm b)
⊢ natNorm (mod a b) < natNorm b