proposition: Lemma Cauchy_Lim_abs : forall seq y, Cauchy_Lim_prop2 seq y -> Cauchy_Lim_prop2 (fun n => AbsIR (seq n)) (AbsIR y).
proof: Proof. intros seq y H. red in |- *; red in H. intros eps He. elim (H eps He); clear H. intros N HN. exists N; intros. apply AbsIR_imp_AbsSmall. cut (AbsIR (seq m[-]y) [<=] eps). intro. 2: apply AbsSmall_imp_AbsIR; apply HN; assumption. cut (seq m[-]y [<=] eps). 2: eapply leEq_transitive; [ apply leEq_AbsIR | apply H0 ]. intro. cut (y[-]seq m [<=] eps). 2: eapply leEq_transitive; [ apply leEq_AbsIR | eapply leEq_wdl; [ apply H0 | apply AbsIR_minus ] ]. intro. simpl in |- *; unfold ABSIR in |- *. apply Max_leEq. apply shift_minus_leEq. apply Max_leEq. apply shift_leEq_plus'. apply leEq_transitive with y. apply shift_minus_leEq; apply shift_leEq_plus'; assumption. apply lft_leEq_Max. apply shift_leEq_plus'. apply leEq_transitive with ( [--]y). apply shift_minus_leEq; apply shift_leEq_plus'. rstepl (y[-]seq m). assumption. apply rht_leEq_Max. astepr ( [--][--]eps); apply inv_resp_leEq. apply shift_leEq_minus; apply shift_plus_leEq'. apply leEq_wdr with (Max (seq m) [--] (seq m) [+]eps). apply Max_leEq. apply leEq_transitive with (seq m[+]eps). apply shift_leEq_plus'; assumption. apply plus_resp_leEq. apply lft_leEq_Max. apply leEq_transitive with ( [--] (seq m) [+]eps). apply shift_leEq_plus'; rstepl (seq m[-]y); assumption. apply plus_resp_leEq. apply rht_leEq_Max. unfold cg_minus in |- *. algebra. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero