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