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