proposition: Lemma lim_const_seq : ∀ (c : ℝ), constant_sequence c ⟶ c.
proof: Proof. Take c : ℝ. Define s := (constant_sequence c). To show: (∀ ε : ℝ, ε > 0 ⇒ ∃ N : ℕ, ∀ n : ℕ, (n ≥ N)%nat ⇒ |(s n) - c| < ε). Take ε : ℝ; such that (ε > 0). Choose Nn := O. Take n : ℕ; such that (n ≥ Nn)%nat. It holds that (s n = c). We conclude that (& |s n - c| = | c - c | = |0| = 0 < ε). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations