theorem Th19: :: INT_4:19

for p, q, n being Nat st n > 0 & p > 0 holds
(p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1)))