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