theorem MD: :: NUMERAL3:44

for a, n being Nat
for b being non zero Nat holds a mod (b |^ n) = a - ((b |^ n) * (a div (b |^ n)))