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