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