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