proposition: Lemma fun_Lim_seq_minus_IR : forall H H', conv_fun_seq'_IR J (fun n => f n{-}g n) (Cauchy_fun_seq_Lim_IR _ _ _ Hf{-}Cauchy_fun_seq_Lim_IR _ _ _ Hg) H H'.
proof: Proof. intros. red in |- *; intros. cut (Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ _ (Hf a b Hab Hinc))); [ intro H0 | Contin ]. cut (Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ _ (Hg a b Hab Hinc))); [ intro H1 | Contin ]. intros. eapply conv_fun_seq'_wdr with (contF := Continuous_I_minus _ _ _ _ _ H0 H1). apply Feq_symmetric; apply Feq_minus; apply Cauchy_fun_seq_Lim_char. apply fun_Lim_seq_minus with (Hf := Hf a b Hab Hinc) (Hg := Hg a b Hab Hinc) (H := fun n : nat => included_imp_Continuous _ _ (H n) _ _ _ Hinc). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions