proposition: Lemma seq_ex_almost_maximizer_ε : ∀ (a : ℕ → ℝ) (pr : has_ub a) (ε : ℝ), ε > 0 ⇒ ∃ k : ℕ, a k > lub a pr - ε.
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists k : ℕ, a k > (let (a0, _) := ub_to_lub a (i) in a0) - ε). Define lub_a_prf := (ub_to_lub a (i)). clear _defeq. Obtain such an l. Take ε : ℝ; such that (ε > 0). By exists_almost_maximizer_ε it holds that (∃ y : ℝ, (EUn a) y ∧ y > l - ε). Obtain such a y. It holds that ((EUn a) y ∧ y > l - ε) (iv). Because (iv) both (EUn a y) and (y > l - ε) hold. It holds that (there exists n : ℕ , y = a n). Obtain such an n. Choose k := n. We need to show that (l - ε < a n). We conclude that (& l - ε < y = a n). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics