proposition: Lemma nonneg_div_four : forall eps : R, [0] [<=] eps -> [0] [<=] eps [/]FourNZ.
proof: Proof. intros. rstepr ((eps [/]TwoNZ) [/]TwoNZ). apply nonneg_div_two; apply nonneg_div_two; assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)