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