proposition: Lemma Lim_seq_eq_Lim_subseq : Lim seq1 [=] Lim seq2.
proof: Proof. cut (Cauchy_Lim_prop2 seq1 (Lim seq2)). 2: apply Cprop2_seq_imp_Cprop2_subseq with (CS_seq _ seq2) f; auto; apply Cauchy_complete. intro. apply eq_symmetric_unfolded. apply Limits_unique; assumption. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero