have h2 := lt_trans one_pos ht
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
⊢ 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
⊢ c < ↑a ∧ 0 < c