α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
⊢ 0 ≤ 1
α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
⊢ 0 ≤ a ^ 0
rw [pow_zero]
no goals
α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
⊢ 0 ≤ 1
exact zero_le_one
α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a * a ^ n
α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
rw [pow_succ]
no goals
α : Type u
β : Type ?u.13277
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a * a ^ n
exact mul_nonneg H (pow_nonneg H _)