proposition: Lemma Cprop2_subseq_imp_Cprop2_seq : forall a, Cauchy_Lim_prop2 seq1 a -> Cauchy_Lim_prop2 seq2 a.
proof: Proof. intros. cut (Cauchy_prop seq1); intros. 2: apply Cauchy_prop2_prop. 2: exists a; assumption. cut (Cauchy_prop seq2); intros H1. 2: apply conv_subseq_imp_conv_seq; assumption. cut (Cauchy_Lim_prop2 (Build_CauchySeq _ _ H1) (Lim (Build_CauchySeq _ _ H1))); intros. 2: apply Cauchy_complete. cut (Cauchy_Lim_prop2 seq1 (Lim (Build_CauchySeq _ _ H1))); intros. 2: apply Cprop2_seq_imp_Cprop2_subseq; assumption. cut (Lim (Build_CauchySeq _ _ H1) [=] a). intro H4. eapply Lim_wd. apply H4. assumption. apply Lim_unique with seq1; assumption. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero