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