proposition: Lemma Lim_less_so : forall (seq : CauchySeq IR) y, Lim seq [<] y -> {eps : IR | [0] [<] eps | {N : nat | forall m, N <= m -> seq m[+]eps [<] y}}.
proof: Proof. intros. elim (Lim_less_so_seq_less seq ((Lim seq[+]y) [/]TwoNZ)). intros x H0. exists ((y[-]Lim seq) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. exists x. intros. apply shift_plus_less. rstepr ((Lim seq[+]y) [/]TwoNZ). apply H0. assumption. apply Smallest_less_Average. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)