Theorem: exercise3_6 (LeanCourse/Assignments/Assignment3.lean)

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
⊢ ∀ (n : ℕ), u n ≤ l
Tactic:
sorry
State after:
no goals