proposition: Lemma nonneg_div_two' : forall eps : R, [0] [<=] eps -> eps [/]TwoNZ [<=] eps.
proof: Proof. intros. apply shift_div_leEq. apply pos_two. astepl (eps[+][0]); rstepr (eps[+]eps). apply plus_resp_leEq_lft; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)