proposition: Lemma shift_minus_less : forall x y z : R, x [<] z[+]y -> x[-]y [<] z.
proof: Proof. intros. astepr (z[+]y[-]y). apply minus_resp_less. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)