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

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

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

end;

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

then reconsider b = b as non zero Integer ;
[\(a / (a * b))/] is weightless ;
hence a div (a * b) is weightless by INT_1:def 9; :: thesis: verum

end;

end;