proposition: Lemma pos_div_four' : forall eps : R, [0] [<] eps -> eps [/]FourNZ [<] eps.
proof: Proof. intros. rstepl ((eps [/]TwoNZ) [/]TwoNZ). apply leEq_less_trans with (eps [/]TwoNZ). 2: apply pos_div_two'; assumption. apply less_leEq. apply pos_div_two'. apply pos_div_two. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)