let a, b, n, k be Nat; :: thesis: a div (b |^ (n + k)) = (a div (b |^ n)) div (b |^ k)
a div ((b |^ n) * (b |^ k)) = (a div (b |^ n)) div (b |^ k) by NAT_2:27;
hence a div (b |^ (n + k)) = (a div (b |^ n)) div (b |^ k) by NEWTON:8; :: thesis: verum