proposition: Lemma plus_resp_leEq_less : forall a b c d : R, a [<=] b -> c [<] d -> a[+]c [<] b[+]d.
proof: Proof. intros. astepl (c[+]a). astepr (d[+]b). apply plus_resp_less_leEq; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)