β : Type ?u.251747
A : Type ?u.251750
G : Type ?u.251753
M : Type ?u.251756
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ 0 ≤ a ^ n * a ^ n
β : Type ?u.251747
A : Type ?u.251750
G : Type ?u.251753
M : Type ?u.251756
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ 0 ≤ a ^ bit0 n
rw [pow_bit0]
no goals
β : Type ?u.251747
A : Type ?u.251750
G : Type ?u.251753
M : Type ?u.251756
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ 0 ≤ a ^ n * a ^ n
exact mul_self_nonneg _