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 div (b |^ n)) mod (b |^ k))
let b be non zero Nat; :: thesis: a div (b |^ n) = ((a div (b |^ (n + k))) * (b |^ k)) + ((a div (b |^ n)) mod (b |^ k))
(a mod (b |^ (n + k))) - (a mod (b |^ n)) = ((a mod (b |^ n)) + (((a div (b |^ n)) mod (b |^ k)) * (b |^ n))) - (a mod (b |^ n)) by ABLK;
then (b |^ n) * ((a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k))) = ((a div (b |^ n)) mod (b |^ k)) * (b |^ n) by RMD;
then (a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k)) = (a div (b |^ n)) mod (b |^ k) by XCMPLX_1:5;
hence a div (b |^ n) = ((a div (b |^ (n + k))) * (b |^ k)) + ((a div (b |^ n)) mod (b |^ k)) ; :: thesis: verum