case a
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}
n : ℕ
⊢ divisorsAntidiagonal 1 = {(1, 1)}
ext
no goals
case a
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}
simp [mul_eq_one, Prod.ext_iff]