proposition: Lemma Lim_subseq_eq_Lim_seq : Lim seq1 [=] Lim seq2.
proof: Proof. cut (Cauchy_Lim_prop2 seq2 (Lim seq1)). 2: exact (Cprop2_subseq_imp_Cprop2_seq seq1 seq2 f monF crescF subseq mon_seq2 _ (Cauchy_complete seq1)). intro. apply Limits_unique; assumption. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero