α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ False
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : n ≠ 0
⊢ 0 < a ^ bit0 n → a ≠ 0
rintro h rfl
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ bit0 n ≠ 0
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ False
refine' (zero_zpow _ _).not_gt h
no goals
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ bit0 n ≠ 0
rwa [bit0_ne_zero]