reconsider c = (max (a,b)) - a as non negative Real ;
not a / (a + c) is heavy ;
hence not a / (max (a,b)) is heavy ; :: thesis: verum