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