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