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