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