proposition: Lemma Lim_minus : forall seq1 seq2 : CauchySeqR, Lim (Build_CauchySeq _ _ (Cauchy_minus seq1 seq2)) [=] Lim seq1[-]Lim seq2.
proof: Proof. intros. apply eq_symmetric_unfolded. apply Limits_unique. simpl in |- *. apply Cauchy_Lim_minus. apply Cauchy_complete. apply Cauchy_complete. Qed.
imports: CoRN.reals.CReals Coq(Lia)