proposition: Lemma seq_ex_almost_maximizer_m : ∀ (a : ℕ → ℝ) (pr : has_ub a) (m : ℕ), ∃ k : ℕ, a k > lub a pr - 1 / (INR(m) + 1).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a). Take m : ℕ. apply seq_ex_almost_maximizer_ε. It holds that (0 < m + 1)%R. We conclude that (1 / (m+1) > 0). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics