proposition: Lemma div_resp_less : forall (x y z : R) z_, [0] [<] z -> x [<] y -> (x[/] z[//]z_) [<] (y[/] z[//]z_).
proof: Proof. intros. rstepl (x[*]([1][/] z[//]z_)). rstepr (y[*]([1][/] z[//]z_)). apply mult_resp_less. assumption. apply recip_resp_pos. auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)