proposition: Lemma Taylor_bnd_trans : forall f g : nat -> PartIR, (forall n x Hx Hx', AbsIR (f n x Hx) [<=] AbsIR (g n x Hx')) -> (forall n, Continuous realline (g n)) -> Taylor_bnd g -> Taylor_bnd f.
proof: Proof. intros f g bndf contg Gbnd r H a b Hab Hinc e H0. elim (Gbnd r (fun n : nat => Continuous_scal _ _ (contg n) _) _ _ _ Hinc e H0); intros N HN. exists N; intros. eapply leEq_transitive. 2: apply HN with (n := n) (Hx := Hx); auto. cut (forall (z t : IR) Ht, AbsIR z [=] AbsIR (z[-][-C-][0] t Ht)); intros. 2: simpl in |- *; apply AbsIR_wd; algebra. eapply leEq_wdl. 2: apply H2. eapply leEq_wdr. 2: apply H2. simpl in |- *. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_lft; auto. apply AbsIR_nonneg. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor