no goals
α : Type ?u.38546
β : Type ?u.38549
ι : Type ?u.38552
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
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_le_seq n _ h _ <;>
  simp [_root_.pow_succ, mul_assoc, le_refl]