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