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