replace ht : 1 < t := by
  rw [← Int.natCast_pos] at h
  have h2 := le_trans Int.one_nonneg (le_of_lt hn)
  rw [Int.lt_iff_add_one_le] at hn h ⊢
  rw [← ht]
  exact le_mul_of_le_of_one_le_of_nonneg hn h h2
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ c < ↑a ∧ 0 < c
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
⊢ c < ↑a ∧ 0 < c