proposition: Lemma FPowerSeries'_comp : forall b, (forall n, AbsIR (b n) [<=] a n) -> fun_series_convergent_IR J (FPowerSeries' x0 b).
proof: Proof. intros. apply fun_comparison_IR with (fun n : nat => FAbs (FPowerSeries' x0 a n)). intros n. apply Included_imp_Continuous with realline;[Contin | auto with *]. auto. intros. apply leEq_wdr with (AbsIR (FPowerSeries' x0 a n x (ProjIR1 Hx'))). 2: apply eq_symmetric_unfolded; apply FAbs_char. simpl in |- *. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_division with (y__ := AbsIR_resp_ap_zero _ (nring_fac_ap_zero IR n)). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_division with (y__ := AbsIR_resp_ap_zero _ (nring_fac_ap_zero IR n)). apply div_resp_leEq. eapply less_leEq_trans. apply (pos_nring_fac IR n). apply leEq_AbsIR. apply leEq_transitive with (a n); [ auto | apply leEq_AbsIR ]. Qed.
imports: CoRN.ftc.FTC