apply Rel.symm (α := ℕ × ℕ)
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m, 0) ≃ (n * m + 0 * 0, n * 0 + 0 * m)
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m + 0 * 0, n * 0 + 0 * m) ≃ (n * m, 0)