proposition: Lemma plus_resp_leEq_both : forall x y a b : R, x [<=] y -> a [<=] b -> x[+]a [<=] y[+]b.
proof: Proof. intros. apply leEq_transitive with (y := x[+]b). rstepl (a[+]x). rstepr (b[+]x). apply plus_resp_leEq. assumption. apply plus_resp_leEq. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)