proposition: Lemma Cauchy_Lim_minus : forall seq1 seq2 y1 y2, Cauchy_Lim_prop2 seq1 y1 -> Cauchy_Lim_prop2 seq2 y2 -> Cauchy_Lim_prop2 (fun n => seq1 n[-]seq2 n) (y1[-]y2).
proof: Proof. intros. unfold cg_minus in |- *. change (Cauchy_Lim_prop2 (fun n : nat => seq1 n[+] (fun m : nat => [--] (seq2 m)) n) (y1[+][--]y2)) in |- *. apply Cauchy_Lim_plus. assumption. apply Cauchy_Lim_inv. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)