for N, M being ExtNat holds
( not N <= M + 1 or N <= M or N = M + 1 )