proposition: Lemma Lim_inv : forall seq : CauchySeqR, Lim (Build_CauchySeq _ _ (Cauchy_inv seq)) [=] [--] (Lim seq).
proof: Proof. intros. apply eq_symmetric_unfolded. apply Limits_unique. simpl in |- *. apply Cauchy_Lim_inv. apply Cauchy_complete. Qed.
imports: CoRN.reals.CReals Coq(Lia)