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