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