proposition: Lemma Cauchy_Lim_prop2_wd' : forall seq1 seq2 c, Cauchy_Lim_prop2 seq1 c -> { N : nat | forall n, N <= n -> seq1 n [=] seq2 n} -> Cauchy_Lim_prop2 seq2 c.
proof: Proof. intros seq1 seq2 c H1 H2. red in |- *. intros eps H3. elim (H1 eps H3). intros M H4. destruct H2 as [N H2]. exists (Nat.max N M) . intros. assert (N <= m); eauto with arith. assert (M <= m); eauto with arith. astepr (seq1 m[-]c). apply H4; auto. Qed.
imports: CoRN.reals.CReals Coq(Lia)