proposition: Lemma seq_lim_lim (x : seq X) (N : Q -> nat) (A : cauchy x N) : seq_lim x (lim (reg_fun A)) (λ e, N (e / 2)).
proof: Proof. set (f := reg_fun A). intros e A1 n A2. apply (mspc_triangle' (e / 2) (e / 2) (x (N (e / 2)))). + field; change ((2 : Q) ≠ 0); solve_propholds. + now apply mspc_symm, A; [solve_propholds | reflexivity |]. + change (x (N (e / 2))) with (f (e / 2)). apply completeness_criterion; solve_propholds. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.theory.setoids MathClasses.theory.products MathClasses.implementations.stdlib_rationals MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum