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