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