let a, b be Nat; :: thesis: a div (b |^ 2) = (a div b) div b
a div (b |^ 2) = a div (b * b) by NEWTON:81
.= (a div b) div b by NAT_2:27 ;
hence a div (b |^ 2) = (a div b) div b ; :: thesis: verum