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