theorem :: COUNTERS:14

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