F : Type ?u.112052
α : Type ?u.112055
β : Type ?u.112058
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < 0
ha : a = 0
⊢ False
F : Type ?u.112052
α : Type ?u.112055
β : Type ?u.112058
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < a ^ n
ha : a = 0
⊢ False
rw [ha, zero_pow h₀] at h
no goals
F : Type ?u.112052
α : Type ?u.112055
β : Type ?u.112058
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < 0
ha : a = 0
⊢ False
exact lt_irrefl 0 h