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