Definition natlehandplus (i j k l : nat) : i ≤ j -> k ≤ l -> i + k ≤ j + l. Proof. intros r s. use (@istransnatleh _ (j + k) _). - apply natlehandplusr. apply r. - apply natlehandplusl. apply s. Defined.