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