proposition: Lemma fun_Cauchy_prop_minus : forall H, Cauchy_fun_seq_IR J (fun n => f n{-}g n) H.
proof: Proof. intro. cut (Continuous J (Cauchy_fun_seq_Lim_IR _ _ _ Hf{-}Cauchy_fun_seq_Lim_IR _ _ _ Hg)); [ intro H0 | Contin ]. apply conv_Cauchy_fun_seq'_IR with (Cauchy_fun_seq_Lim_IR _ _ _ Hf{-}Cauchy_fun_seq_Lim_IR _ _ _ Hg) H0. apply fun_Lim_seq_minus_IR. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions