no goals
m n k : ℕ
h : k < m
hk : optParam (k < m + n) (_ : k < m + n)
hnk : optParam (n + k < n + m) (_ : n + k < n + m)
⊢ ↑finAddFlip { val := k, isLt := hk } = { val := n + k, isLt := hnk }
convert finAddFlip_apply_castAdd ⟨k, h⟩ n