simp [normSq, Norm]
case mk
b c : ℤω
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { x := x, y := y }) = ↑(norm { x := x, y := y })
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re * (↑inclusion { x := x, y := y }).re +
      (↑inclusion { x := x, y := y }).im * (↑inclusion { x := x, y := y }).im =
    ↑(norm { x := x, y := y })