proposition: Lemma fun_lim_seq_derivative : Derivative J pJ F G.
proof: Proof. elim (nonvoid_point _ (proper_nonvoid _ pJ)); intros a Ha. set (h := fun n : nat => ( [-S-]contg n) a Ha) in *. set (H := ( [-S-]contG) a Ha) in *. assert (H0 : Derivative J pJ H G). unfold H in |- *; apply FTC1. assert (H1 : forall n : nat, Derivative J pJ (h n) (g n)). intro; unfold h in |- *; apply FTC1. assert (H2 : conv_fun_seq'_IR J _ _ (fun n : nat => Derivative_imp_Continuous _ _ _ _ (H1 n)) (Derivative_imp_Continuous _ _ _ _ H0)). unfold h, H in |- *. eapply fun_lim_seq_integral_IR with (contf := contg); auto. cut {c : IR | Feq J (F{-}H) [-C-]c}. intro H3. elim H3; clear H3; intros c Hc. apply Derivative_wdl with (H{+} [-C-]c). apply Feq_transitive with (H{+} (F{-}H)). apply Feq_plus. apply Feq_reflexive; Included. apply Feq_symmetric; assumption. clear Hc H2 H1; clearbody H. FEQ. apply Derivative_wdr with (G{+} [-C-][0]). FEQ. apply Derivative_plus; auto. apply Derivative_const. assert (H3 : forall n : nat, {c : IR | Feq J (f n{-}h n) [-C-]c}). intro; apply FConst_prop with pJ. apply Derivative_wdr with (g n{-}g n). FEQ. apply Derivative_minus; auto. assert (contw : forall n : nat, Continuous J (f n{-}h n)). unfold h in |- *; Contin. assert (contW : Continuous J (F{-}H)). unfold H in |- *; Contin. apply fun_const_Lim with (fun n : nat => f n{-}h n) contw contW. auto. eapply fun_Lim_seq_minus'_IR. apply convF. apply H2. assumption. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems