for a, b being positive Real st a - b = a * b holds
b is light