let a be Nat; :: thesis: for b being non trivial Nat holds a div (b |^ 2) = ((a div (b |^ 0)) - (a mod (b |^ 2))) div (b |^ 2)
let b be non trivial Nat; :: thesis: a div (b |^ 2) = ((a div (b |^ 0)) - (a mod (b |^ 2))) div (b |^ 2)
a mod (b |^ 2) = a - ((b |^ 2) * (a div (b |^ 2))) by MD;
then a div (b |^ 2) = ((a div (1 * (b |^ 0))) - (a mod (b |^ 2))) div (b |^ 2) ;
hence a div (b |^ 2) = ((a div (b |^ 0)) - (a mod (b |^ 2))) div (b |^ 2) ; :: thesis: verum