β : Type ?u.215364
A : Type ?u.215367
G : Type ?u.215370
M : Type ?u.215373
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
β : Type ?u.215364
A : Type ?u.215367
G : Type ?u.215370
M : Type ?u.215373
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1
rw [pow_succ]
no goals
β : Type ?u.215364
A : Type ?u.215367
G : Type ?u.215370
M : Type ?u.215373
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one _ h₀ h₁.le)