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