per cases ( b = 0 or b <> 0 ) ;

suppose b = 0 ; :: thesis: b div (a * b) is zero

hence b div (a * b) is zero ; :: thesis: verum

end;

suppose B1: b <> 0 ; :: thesis: b div (a * b) is zero

b div (b * a) = (b div b) div a by PRE_FF:5
.= 1 div a by B1, INT_1:49 ;
hence b div (a * b) is zero ; :: thesis: verum

end;

end;