proposition: Lemma conv_evt_eq_seq : ∀ (a b : ℕ → ℝ) (l : ℝ), (evt_eq_sequences a b) ⇒ (a ⟶ l) ⇒ (b ⟶ l).
proof: Proof. Take a, b : (ℕ → ℝ) and l : ℝ. Assume that (evt_eq_sequences a b) (i) and (a ⟶ l). We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ |b n - l| < ε ). Take ε : ℝ; such that (ε > 0). It holds that (there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ |a n - l| < ε). Obtain such an N1. By (i) it holds that (there exists K : nat, for all n : ℕ, (n ≥ K)%nat ⇨ a n = b n). Obtain such a K. Choose M := (Nat.max N1 K). Take n : ℕ; such that (n ≥ M)%nat. It holds that (b n = a n). We conclude that (& |b n - l| = |a n - l| < ε). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations