for N, M, K being ExtNat st N <= M holds
N <= M + K