proposition: Lemma Cauchy_plus : forall seq1 seq2 : CauchySeqR, Cauchy_prop (fun n => seq1 n [+] seq2 n).
proof: Proof. intros. apply Cauchy_prop2_prop. unfold Cauchy_prop2 in |- *. exists (Lim seq1[+]Lim seq2). apply Cauchy_Lim_plus. apply Cauchy_complete. apply Cauchy_complete. Qed.
imports: CoRN.reals.CReals Coq(Lia)