proposition: Lemma pos_div_three' : forall eps : R, [0] [<] eps -> eps [/]ThreeNZ [<] eps.
proof: Proof. intros. apply mult_cancel_less with (Three:R). apply pos_three. rstepl (eps[+][0]); rstepr (eps[+]Two[*]eps). apply plus_resp_less_lft. apply mult_resp_pos; auto. apply pos_two. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)