proposition: Lemma aew_Lim : Lim x [=] Lim y.
proof: Proof. intros. cut (Cauchy_Lim_prop2 x (Lim y)). intro. apply eq_symmetric_unfolded. apply Limits_unique; assumption. apply aew_Cauchy2 with (y:nat -> IR). elim aew_equal; intros n Hn; exists n; intros. apply eq_symmetric_unfolded; apply Hn; auto. apply Cauchy_complete. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)