proposition: Lemma AbsSmall_x_minus_eps_div2 : forall x eps : R, [0] [<=] eps -> AbsSmall eps (x[-] (x[-]eps [/]TwoNZ)).
proof: Proof. intros. apply AbsSmall_x_minus_delta. assumption. apply nonneg_div_two. assumption. apply eps_div_leEq_eps. assumption. apply less_leEq. apply one_less_two. Qed.
imports: CoRN.algebra.COrdFields2