β : Type ?u.202613
A : Type ?u.202616
G : Type ?u.202619
M : Type ?u.202622
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m n : ℕ
⊢ 0 ≤ 1
β : Type ?u.202613
A : Type ?u.202616
G : Type ?u.202619
M : Type ?u.202622
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m n : ℕ
⊢ 0 ^ (n + 1) ≤ 1
rw [zero_pow n.succ_pos]
no goals
β : Type ?u.202613
A : Type ?u.202616
G : Type ?u.202619
M : Type ?u.202622
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m n : ℕ
⊢ 0 ≤ 1
exact zero_le_one