β : Type ?u.234679
A : Type ?u.234682
G : Type ?u.234685
M : Type ?u.234688
R : Type u_1
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ 0 < (a * a) ^ n
β : Type ?u.234679
A : Type ?u.234682
G : Type ?u.234685
M : Type ?u.234688
R : Type u_1
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ 0 < a ^ bit0 n
rw [pow_bit0']
no goals
β : Type ?u.234679
A : Type ?u.234682
G : Type ?u.234685
M : Type ?u.234688
R : Type u_1
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
n : ℕ
⊢ 0 < (a * a) ^ n
exact pow_pos (mul_pos_of_neg_of_neg ha ha) _