n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.snd + c
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ kl.snd ≤ n
rw [le_iff_exists_add]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.snd + kl.fst
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.snd + c
use kl.1
no goals
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.snd + kl.fst
rwa [mem_antidiagonal, eq_comm, add_comm] at hlk