proposition: Lemma seq_lim_unique : ∀ (x : seq X) (a1 a2 : X) N1 N2, seq_lim x a1 N1 → seq_lim x a2 N2 → a1 = a2.
proof: Proof. intros x a1 a2 N1 N2 A1 A2. apply -> mspc_eq; intros q A. assert (A3 : 0 < q / 2) by solve_propholds. specialize (A1 (q / 2) A3); specialize (A2 (q / 2) A3). set (M := Peano.max (N1 (q / 2)) (N2 (q / 2))). assert (A4 : N1 (q / 2) ≤ M) by apply Nat.le_max_l. assert (A5 : N2 (q / 2) ≤ M) by apply Nat.le_max_r. specialize (A1 M A4); specialize (A2 M A5). apply mspc_symm in A1. apply (mspc_triangle' (q / 2) (q / 2) (x M)); trivial. field; change ((2 : Q) ≠ 0); 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