proposition: Lemma seq_ordered_lim_ordered : ∀ (a b: ℕ → ℝ) (m l : ℝ), Un_cv a m ⇒ Un_cv b l ⇒ (∀ n : ℕ, a n ≤ b n) ⇒ m ≤ l.
proof: Proof. Take a : (ℕ → ℝ). Take b : (ℕ → ℝ). Take m : ℝ. Take l : ℝ. Assume that (Un_cv a m) and (Un_cv b l). Assume that (∀ n : ℕ, a n ≤ b n). We argue by contradiction. Assume that (~ m <= l). It holds that (l < m). Define ε := ((m - l)/2). It holds that (ε > 0). It holds that (for all eps : ℝ, eps > 0 ⇨ there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ ｜ a n - m ｜ < eps). It holds that (for all eps : ℝ, eps > 0 ⇨ there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ ｜ b n - l ｜ < eps). It holds that (∃ N1 : ℕ, ∀ n : ℕ, (n ≥ N1)%nat ⇒ R_dist (a n) m < ε). Obtain such an N1. It holds that (∃ N2 : ℕ, ∀ n : ℕ, (n ≥ N2)%nat ⇒ R_dist (b n) l < ε). Obtain such an N2. Define N3 := (Nat.max N1 N2). We claim that (b N3 < a N3). { It holds that (|b(N3) - l| < ε). It holds that (|a(N3) - m| < ε). By Rabs_def2 it holds that (a N3 - m < ε ∧ - ε < a N3 - m). By Rabs_def2 it holds that (b N3 - l < ε ∧ - ε < b N3 - l). We conclude that (& b N3 < l + ε = l + (m - l)/2 = m - (m - l)/2 = m - ε < a N3). } It holds that (a N3 <= b N3). Contradiction. Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations