let a, n, k be Nat; :: thesis: for b being non zero Nat holds b |^ n divides (a mod (b |^ (n + k))) - (a mod (b |^ n))
let b be non zero Nat; :: thesis: b |^ n divides (a mod (b |^ (n + k))) - (a mod (b |^ n))
(a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k))))) by DMK;
hence b |^ n divides (a mod (b |^ (n + k))) - (a mod (b |^ n)) ; :: thesis: verum