proposition: Lemma plus_resp_leEq : forall x y z : R, x [<=] y -> x[+]z [<=] y[+]z.
proof: Proof. intros x y z. do 2 rewrite -> leEq_def. intros. intro. apply H. apply (plus_cancel_less _ _ _ _ X). Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)