exact pow_pos h 2
case intro.intro.intro.intro.intro.right
a b : ℕ
t : ℤ
h0 : t * ↑a - 1 < t * ↑b - 1
h : 0 < t * ↑a - 1
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
ht : 1 < t
h3 : ∀ (x y : ℤ), x < y ↔ t * x - 1 < t * y - 1
h2 : ∀ (x : ℤ), 0 < x ↔ 0 < t * x - 1
⊢ 0 < (t * ↑a - 1) ^ 2
no goals