theorem :: COUNTERS:17

for N, M being ExtNat st N * M = 1 holds
N = 1