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