proposition: Lemma CV_minus : forall (An Bn:nat -> R) (l1 l2:R), Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2).
proof: Proof. intros. replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). - unfold Rminus; apply CV_plus. + assumption. + apply CV_opp; assumption. - unfold Rminus, opp_seq; reflexivity. Qed.
imports: Rbase Rfunctions Rseries Lia