proposition: Lemma exists_almost_lim_sup_aux : ∀ (a : ℕ → ℝ) (pr : has_ub a) (m : ℕ) (N : ℕ), ∃ k : ℕ, (k ≥ N)%nat ∧ a k > sequence_ub a pr N - 1 / (INR(m) + 1).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). Take m, Nn : ℕ. By seq_ex_almost_maximizer_m it holds that (∃ k : ℕ, a (Nn + k)%nat > sequence_ub a (i) Nn - 1 / (INR m + 1)). Obtain such a k. Choose l := (Nn+k)%nat. We show both statements. - We need to show that (l ≥ Nn)%nat. We conclude that (l ≥ Nn)%nat. - We need to show that ( a l > sequence_ub a (i) Nn - 1 / (m + 1) ). We conclude that ( a l > sequence_ub a (i) Nn - 1 / (m + 1) ). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics