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