x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z
x y z : ℤ
⊢ PythagoreanTriple x y z ↔ PythagoreanTriple y x z
delta PythagoreanTriple
no goals
x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z
rw [add_comm]