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