proposition: Lemma shift_mult_leEq : forall (x y z : R) z_, [0] [<] z -> x [<=] (y[/] z[//]z_) -> x[*]z [<=] y.
proof: Proof. intros. rstepr ((y[/] z[//]z_) [*]z). apply mult_resp_leEq_rht; [ assumption | apply less_leEq; assumption ]. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)