Theorem: LoVe.Int.Setoid_Iff (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
pn₁ pn₂ : ℕ × ℕ
⊢ pn₁ ≈ pn₂ ↔ pn₁.fst + pn₂.snd = pn₂.fst + pn₁.snd
Tactic:
rfl
State after:
no goals