proposition: Lemma Lim_abs : forall seq : CauchySeq IR, Lim (Build_CauchySeq _ _ (Cauchy_abs seq)) [=] AbsIR (Lim seq).
proof: Proof. intros. apply eq_symmetric_unfolded; apply Limits_unique. simpl in |- *; apply Cauchy_Lim_abs. apply Cauchy_complete. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero