proposition: Lemma CS_seq_plus : Cauchy_prop (fun m => f m[+]g m).
proof: Proof. unfold Cauchy_prop in |- *. intros. set (e_div_4 := e [/]FourNZ) in *. cut ([0] [<] e_div_4); [ intro Heps | unfold e_div_4 in |- *; apply pos_div_four; auto ]. unfold Cauchy_prop in Hf. unfold Cauchy_prop in Hg. elim (Hf e_div_4 Heps); intros N1 H21. elim (Hg e_div_4 Heps); intros N2 H31. exists (Nat.max N1 N2). intros. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). rstepr (f m[-]f (Nat.max N1 N2)[+](g m[-]g (Nat.max N1 N2))). apply AbsSmall_plus. rstepr (f m[-]f N1[+](f N1[-]f (Nat.max N1 N2))). rstepl (e [/]FourNZ[+]e [/]FourNZ). apply AbsSmall_plus. apply H21; eauto with arith. apply AbsSmall_minus. apply H21; eauto with arith. rstepr (g m[-]g N2[+](g N2[-]g (Nat.max N1 N2))). rstepl (e [/]FourNZ[+]e [/]FourNZ). apply AbsSmall_plus. apply H31; eauto with arith. apply AbsSmall_minus. apply H31; eauto with arith. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)