proposition: Lemma Derivative_FPowerSeries1' : forall H, Derivative J H (FSeries_Sum Hf) (FSeries_Sum Hg).
proof: Proof. intro. eapply Derivative_wdr. apply Feq_symmetric; apply (insert_series_sum _ _ Hg). apply Derivative_FSeries. intro; case n; clear n; intros. simpl in |- *. apply Derivative_wdl with (Fconst (S:=IR) (a 0)). FEQ. Deriv. simpl in |- *. Opaque nring fact. unfold F, G, FPowerSeries' in |- *; simpl in |- *. Derivative_Help. apply eq_imp_Feq. apply included_FScalMult; apply included_FScalMult. apply included_FMult; Included. apply included_FScalMult; Included. intros; simpl in |- *. set (y := nexp _ n (x[-]x0)) in *. rstepl (a (S n) [*]y[*](nring (S n) [/] _[//]nring_fac_ap_zero _ (S n))). rstepr (a (S n) [*]y[*] (nring (S n) [/] _[//] mult_resp_ap_zero _ _ _ (pos_ap_zero _ _ (pos_nring_S _ n)) (nring_fac_ap_zero _ n))). apply mult_wdr. apply div_wd; algebra. Step_final (nring (R:=IR) (S n * fact n)). Qed.
imports: CoRN.ftc.FTC