have h3 : ∀ x y : ℤ, x < y ↔ t * x - 1 < t * y - 1 :=
  λ x y ↦ by rw [sub_lt_sub_iff_right, ← mul_lt_mul_left h2]
case intro.intro.intro.intro.intro
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
⊢ c < ↑a ∧ 0 < c
case intro.intro.intro.intro.intro
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h2 : 0 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
⊢ c < ↑a ∧ 0 < c