proposition: Lemma Taylor_Series_conv_lemma3 : forall a' b d c e a'' x : IR, a' [=] a'' -> x [=] b[*]e -> [0] [<=] e -> forall Hb He Hx, (AbsIR (a'[*] ([1][/] b[//]Hb) [*]c[*]d) [/] e[//]He) [=] AbsIR ((a''[/] x[//]Hx) [*] (c[*]d)).
proof: Proof. intros. astepr (AbsIR ((a''[/] x[//]Hx) [*]c[*]d)). apply eq_transitive_unfolded with (AbsIR a'[*] ([1][/] _[//]AbsIR_resp_ap_zero _ Hb) [*]AbsIR c[*]AbsIR d[/] e[//]He). apply div_wd; algebra. repeat (eapply eq_transitive_unfolded; [ apply AbsIR_resp_mult | apply mult_wdl ]). eapply eq_transitive_unfolded; [ apply AbsIR_resp_mult | apply mult_wdr ]. apply AbsIR_recip. rstepl ((AbsIR a'[/] _[//]mult_resp_ap_zero _ _ _ (AbsIR_resp_ap_zero _ Hb) He) [*] AbsIR c[*]AbsIR d). apply eq_symmetric_unfolded. repeat (eapply eq_transitive_unfolded; [ apply AbsIR_resp_mult | apply mult_wdl ]). eapply eq_transitive_unfolded; [ apply AbsIR_division with (y__ := AbsIR_resp_ap_zero _ Hx) | apply div_wd; algebra ]. eapply eq_transitive_unfolded. 2: apply AbsIR_mult_pos; auto. algebra. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor