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

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