exact ⟨c, eq_sub_of_add_eq h1⟩
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
X : ∀ (m : ℤ), t * m - 1 ≡ -1 [ZMOD t]
c : ℤ
h1 : k + 1 = t * c
⊢ ∃ c, k = t * c - 1
no goals