proposition: Lemma conv_subseq_imp_conv_seq : Cauchy_prop seq1 -> Cauchy_prop seq2.
proof: Proof. intro H. red in |- *; red in H. intros e H0. elim (H e H0). intros N HN. exists (f N). intros. elim (unbnd_f m); intros i Hi. apply AbsIR_imp_AbsSmall. apply leEq_transitive with (AbsIR (seq2 (f i) [-]seq2 (f N))). elim mon_seq2; intro. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (seq2 (f N)); apply H2; assumption. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (seq2 (f N)); apply H2; apply Nat.le_trans with m; auto with arith. apply minus_resp_leEq. apply H2; auto with arith. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_inv_x. 2: apply shift_minus_leEq; astepr (seq2 (f N)); auto. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_inv_x. 2: apply shift_minus_leEq; astepr (seq2 (f N)); apply H2; apply Nat.le_trans with m; auto with arith. apply inv_resp_leEq; apply minus_resp_leEq. apply H2; auto with arith. apply leEq_wdl with (AbsIR (seq1 i[-]seq1 N)). apply AbsSmall_imp_AbsIR; apply HN. apply Nat.lt_le_incl. apply mon_F'; apply Nat.le_lt_trans with m; auto. apply AbsIR_wd; algebra. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero