rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ c < k + c + 1