proposition: Lemma Cauchy_Lim_prop2_wd : forall seq1 seq2 c, Cauchy_Lim_prop2 seq1 c -> (forall n, seq1 n [=] seq2 n) -> Cauchy_Lim_prop2 seq2 c.
proof: Proof. intros. apply Cauchy_Lim_prop2_wd' with seq1; auto. exists 0. auto. Qed.
imports: CoRN.reals.CReals Coq(Lia)