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