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