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