proposition: Lemma shift_leEq_div : forall (x y z : R) y_, [0] [<] y -> x[*]y [<=] z -> x [<=] (z[/] y[//]y_).
proof: Proof. intros x y z H X. repeat rewrite -> leEq_def. intros H0 H1. apply H0. astepr (y[*]x). apply shift_less_mult' with H; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)