rw [complexω_sq]
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * (-complexω - 1)