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