proposition: Lemma low_bd_seq_is_low_bd_lim : ∀ (a : ℕ → ℝ) (L M: ℝ), (∀ n : ℕ, a n ≥ M) ⇒ (Un_cv a L) ⇒ L ≥ M.
proof: Proof. Take a : (ℕ → ℝ). Take L : ℝ. Take M : ℝ. Assume that (∀ n : ℕ, a n ≥ M). Define b := (opp_seq a). Assume that (Un_cv a L). It holds that (b = (fun n => - a n)). By CV_opp it holds that (Un_cv b (-L)). We claim that (-L ≤ -M). { By upp_bd_seq_is_upp_bd_lim it suffices to show that (for all n : ℕ, b n ≤ - M). Take n : ℕ. We conclude that (& b n = - a n <= -M). } We conclude that (L >= M). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations