theorem Lemma167A: :: NUMBER18:71

for m, n being non zero Nat st n > ((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1) holds
ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)