for n, k, p being Nat st 0 < k & (2 * k) |^ k <= n & n |^ k < p holds
( ((p + 1) |^ n) mod (p |^ (k + 1)) > 0 & k ! < (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) & (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1 )