proposition: Lemma Lim_less_so_seq_less : forall (seq : CauchySeq IR) y, Lim seq [<] y -> {N : nat | forall m, N <= m -> seq m [<] y}.
proof: Proof. intros. elim (Cauchy_complete seq ((y[-]Lim seq) [/]TwoNZ)). intro N. intros H0. split with N. intros m H1. generalize (H0 _ H1); intro H2. unfold AbsSmall in H2. elim H2. intros H3 H4. apply plus_cancel_less with ([--] (Lim seq)). eapply leEq_less_trans. apply H4. apply pos_div_two'. apply shift_less_plus; rstepl (Lim seq); auto. apply pos_div_two. apply shift_less_minus; astepl (Lim seq); auto. Qed.
imports: CoRN.reals.CReals Coq(Lia)