proposition: Lemma abs_Taylor_Rem_char : forall n H x Hx Hx' Hx'', AbsIR (F x Hx[-]FSum0 (S n) Taylor_Series x Hx') [=] AbsIR (Taylor_Rem J pJ F a x Ha Hx'' n H).
proof: Proof. intros; apply AbsIR_wd; apply Taylor_Rem_char. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor