proposition: Lemma nonneg_div_three : forall eps : R, [0] [<=] eps -> [0] [<=] eps [/]ThreeNZ.
proof: Proof. intros. apply mult_cancel_leEq with (Three:R). apply pos_three. astepl ([0]:R); rstepr eps. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)