rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
case mk
m k : ℕ
hk : k < m + 1
⊢ m - (m + (m + 1 - ↑⟨k, hk⟩)) % (m + 1) = ↑⟨k, hk⟩
case mk
m k : ℕ
hk✝ : k < m + 1
hk : ∃ c, m = k + c
⊢ m - (m + (m + 1 - ↑⟨k, hk✝⟩)) % (m + 1) = ↑⟨k, hk✝⟩