α : Type ?u.303316
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 j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ j ≤ a ^ i
α : Type ?u.303316
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 j : ℕ
hij : i ≤ j
⊢ a ^ j ≤ a ^ i
let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hij
α : Type ?u.303316
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 j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ (i + k) ≤ a ^ i
α : Type ?u.303316
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 j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ j ≤ a ^ i
rw [hk]
no goals
α : Type ?u.303316
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 j : ℕ
hij : i ≤ j
k : ℕ
hk : j = i + k
⊢ a ^ (i + k) ≤ a ^ i
exact pow_le_pow_of_le_one_aux h ha _ _