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