theorem :: NUMBER08:48

for n being odd Nat holds n divides (2 |^ (n !)) - 1