congr
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + (-(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω) =
    ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + ↑y✝¹ * ↑y✝ * complexω ^ 2
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2