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