"if x and y are doubles and x > y, then we have shown that double_as_int64(x) > double_as_int64(y)"

This only applies for numbers of the same sign though. As soon as the sign changes, the relation breaks since floating point numbers use an independent sign bit while int64 is 2's complement.