theorem :: COUNTERS:13

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