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

suppose b = 0 ; :: thesis: not a / (a * b) is heavy

hence not a / (a * b) is heavy ; :: thesis: verum

end;

suppose b < 0 ; :: thesis: not a / (a * b) is heavy

then reconsider b = b as negative Integer ;

per cases ( a is positive or a is negative ) ;

suppose a is positive ; :: thesis: not a / (a * b) is heavy

then reconsider a = a as positive Integer ;
not b is light ;
then b <= - 1 by TA1;
then a * b <= a * (- 1) by XREAL_1:64;
then a / (a * b) >= a / (- a) by XREAL_1:119;
then a / (a * b) >= - 1 by XCMPLX_1:198;
hence not a / (a * b) is heavy by TA1; :: thesis: verum

end;

suppose a is negative ; :: thesis: not a / (a * b) is heavy

then reconsider a = a as negative Integer ;
not b is light ;
then b <= - 1 by TA1;
then a * b >= a * (- 1) by XREAL_1:65;
then a / (a * b) >= a / (- a) by XREAL_1:120;
then a / (a * b) >= - 1 by XCMPLX_1:198;
hence not a / (a * b) is heavy by TA1; :: thesis: verum

end;

end;

end;

suppose b > 0 ; :: thesis: not a / (a * b) is heavy

then reconsider b = b as positive Integer ;

per cases ( a is positive or a is negative ) ;

suppose a is positive ; :: thesis: not a / (a * b) is heavy

then reconsider a = a as positive Integer ;
not b is light ;
then a * b >= a * 1 by XREAL_1:64;
then a / (a * b) <= a / a by XREAL_1:118;
hence not a / (a * b) is heavy by XCMPLX_1:60; :: thesis: verum

end;

suppose a is negative ; :: thesis: not a / (a * b) is heavy

then reconsider a = a as negative Integer ;
not b is light ;
then a * b <= a * 1 by XREAL_1:65;
then a / (a * b) <= a / a by XREAL_1:121;
hence not a / (a * b) is heavy by XCMPLX_1:60; :: thesis: verum

end;

end;

end;

end;