exact Int.eq_one_of_mul_eq_one_right (le_of_lt h2) h4
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
x : ℤ
h4 : t * x = 1
⊢ t = 1
no goals