proposition: Lemma Lim_wd : forall (seq : nat -> IR) x y, x [=] y -> Cauchy_Lim_prop2 seq x -> Cauchy_Lim_prop2 seq y.
proof: Proof. intros seq x y H H0. red in |- *; red in H0. intros eps H1. elim (H0 _ H1). intros N HN. exists N. intros. astepr (seq m[-]x). apply HN; assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)