proposition: Lemma conv_seq_imp_conv_subseq : Cauchy_prop seq2 -> Cauchy_prop seq1.
proof: Proof. intro H. apply Cauchy_prop2_prop. cut (Cauchy_prop2 (Build_CauchySeq _ _ H)). intro H0. elim H0; intros a Ha; exists a. apply Cprop2_seq_imp_Cprop2_subseq. assumption. exists (Lim (Build_CauchySeq _ _ H)). apply Lim_Cauchy. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero