proposition: Lemma Cauchy_prop_wd' : forall seq1 seq2 : nat -> IR, Cauchy_prop seq1 -> {N : nat | forall n, N <= n -> seq1 n [=] seq2 n} -> Cauchy_prop seq2.
proof: Proof. intros seq1 seq2 H H0. red in |- *. intros e H1. elim (H (e[/]TwoNZ) (pos_div_two IR e H1)). intros N Hn. destruct H0 as [M H0]. exists (Nat.max M N). intros. astepr (seq1 m[-]seq1 (Nat.max M N)). astepr ((seq1 m[-]seq1 N)[+](seq1 N [-]seq1 (Nat.max M N))). apply AbsSmall_eps_div_two. apply Hn. eauto with arith. apply AbsSmall_minus. apply Hn. eauto with arith. rational. apply cg_minus_wd; apply H0; eauto with arith. Qed.
imports: CoRN.reals.CReals Coq(Lia)