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