for a, b being non zero Real holds
( sgn ((1 / a) - (1 / b)) = sgn (b - a) iff sgn b = sgn a )