no goals
α : Type ?u.301195
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : StrictOrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i : ℕ
⊢ a ^ (i + 0) ≤ a ^ i
simp
α : Type ?u.301195
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : StrictOrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i k : ℕ
⊢ a * a ^ (i + k) ≤ 1 * a ^ i
α : Type ?u.301195
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : StrictOrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i k : ℕ
⊢ a ^ (i + (k + 1)) ≤ a ^ i
rw [← add_assoc, ← one_mul (a ^ i), pow_succ]
no goals
α : Type ?u.301195
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : StrictOrderedSemiring R
a : R
h : 0 ≤ a
ha : a ≤ 1
i k : ℕ
⊢ a * a ^ (i + k) ≤ 1 * a ^ i
exact mul_le_mul ha (pow_le_pow_of_le_one_aux h ha _ _) (pow_nonneg h _) zero_le_one