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