proposition: Lemma Lim_unique : forall seq x y, Cauchy_Lim_prop2 seq x -> Cauchy_Lim_prop2 seq y -> x [=] y.
proof: Proof. intros. cut (Cauchy_prop seq); [ intro | apply Cauchy_prop2_prop; exists y; auto ]. apply eq_transitive_unfolded with (Lim (Build_CauchySeq _ _ X1)). apply Limits_unique; auto. apply eq_symmetric_unfolded; apply Limits_unique; auto. Qed.
imports: CoRN.reals.CReals Coq(Lia)