proposition: Lemma plus_cancel_leEq_rht : 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_leEq. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)