proposition: Lemma AbsSmall_x_plus_eps_div2 : forall x eps : R, [0] [<=] eps -> AbsSmall eps (x[-] (x[+]eps [/]TwoNZ)).
proof: Proof. intros. apply AbsSmall_x_plus_delta. assumption. apply nonneg_div_two. assumption. apply nonneg_div_two'. assumption. Qed.
imports: CoRN.algebra.COrdFields2