case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(↑(Fin.natAdd m) { val := k - m, isLt := (_ : k - m < n) })

m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k < n + m
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ ↑finAddFlip { val := k, isLt := h₂ } = { val := k - m, isLt := (_ : k - m < n + m) }
convert @finAddFlip_apply_natAdd n ⟨k - m, (tsub_lt_iff_right h₁).2 ?_⟩ m
no goals
case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(↑(Fin.natAdd m) { val := k - m, isLt := (_ : k - m < n) })
simp [add_tsub_cancel_of_le h₁]
no goals
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k < n + m
rwa [add_comm]