proposition: Lemma Cauchy_abs : forall seq : CauchySeq IR, Cauchy_prop (fun n => AbsIR (seq n)).
proof: Proof. intro. apply Cauchy_prop2_prop. exists (AbsIR (Lim seq)). apply Cauchy_Lim_abs. apply Cauchy_complete. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero