proposition: Lemma nonneg_div_three' : forall eps : R, [0] [<=] eps -> eps [/]ThreeNZ [<=] eps.
proof: Proof. intros. apply shift_div_leEq. apply pos_three. rstepl (eps[+][0][+][0]); rstepr (eps[+]eps[+]eps). repeat apply plus_resp_leEq_both; auto. apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)