proposition: Lemma div_resp_leEq : 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_leEq_rht. assumption. apply less_leEq. apply recip_resp_pos. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)