proposition: Lemma shift_mult_less : forall (x y z : R) y_, [0] [<] y -> x [<] (z[/] y[//]y_) -> x[*]y [<] z.
proof: Proof. intros. astepr ((z[/] y[//]y_)[*]y). apply mult_resp_less; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)