proposition: Lemma div_resp_pos : forall (x y : R) x_, [0] [<] x -> [0] [<] y -> [0] [<] (y[/] x[//]x_).
proof: Proof. intros. astepl ([0][/] x[//]x_). apply div_resp_less_rht; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)