reconsider c = max (a,b) as positive Real ;
( max (a,b) >= a & a >= min (a,b) ) by XXREAL_0:17, XXREAL_0:25;
then max (a,b) >= min (a,b) by XXREAL_0:2;
then (min (a,b)) / c <= (1 * c) / c by XREAL_1:72;
hence not (min (a,b)) / (max (a,b)) is heavy by XCMPLX_1:89; :: thesis: verum