no goals
α : Type ?u.289091
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
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
⊢ 1 + ↑0 * a ≤ (1 + a) ^ 0
simp
no goals
α : Type ?u.289091
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
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
⊢ 1 + ↑1 * a ≤ (1 + a) ^ 1
simp
no goals
α : Type ?u.289091
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
Hsq : 0 ≤ a * a
Hsq' : 0 ≤ (1 + a) * (1 + a)
H : 0 ≤ 2 + a
n : ℕ
this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a
⊢ (1 + a) * (1 + a) * (1 + a) ^ n = (1 + a) ^ (n + 2)
simp only [pow_succ, mul_assoc]