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