α : Type ?u.37075
β : Type ?u.37078
ι : Type ?u.37081
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ u 0 ≤ c ^ 0 * u 0

α : Type ?u.37075
β : Type ?u.37078
ι : Type ?u.37081
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ ∀ (k : ℕ), k < n → c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
α : Type ?u.37075
β : Type ?u.37078
ι : Type ?u.37081
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ u n < c ^ n * u 0
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _
no goals
α : Type ?u.37075
β : Type ?u.37078
ι : Type ?u.37081
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ u 0 ≤ c ^ 0 * u 0
simp
no goals
α : Type ?u.37075
β : Type ?u.37078
ι : Type ?u.37081
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ ∀ (k : ℕ), k < n → c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
simp [_root_.pow_succ, mul_assoc, le_refl]