[lisael]

To elaborate on the 'nice little shortcut' you mentioned, here it is:

If a==b and N≠0, then x==y

EDIT: Formatting

[ummonk]

No, that is not necessary.

"Given an x, y, and N such that x/N == y/N, it is true that x == y".

There is no need to say N != 0 under the ordinary definition of division.