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