Assuming that a and b are two IEEE-754 finite FP numbers of the same type, and a != b is true, does it always hold that a-b != 0? In other words, does a-b==0 for finite a, b imply that a == b?
In IEEE-754 arithmetic, for finite a and b, a == b if and only if a-b == 0. This is specifically why subnormal numbers were included in the IEEE-754 number system.
Not all languages or implementations of languages conform to IEEE-754. Even if they use IEEE-754 formats, they might not strictly use IEEE-754 operations.