[leereeves]

> (x / y) * y equals x

Even without Pony's assumption, that's only true when y != 0.

[umanwizard]

Yeah, (x/y)*y = x is true whenever it's a meaningful statement. x/y has no meaning in standard mathematics when y=0. 1/0 isn't infinity or anything else in standard math, it's literally un-grammatical nonsense.

[chess19]

It should be true for every y that is allowed in the denominator.

That is how fractions are handled in higher math. (Either called "localization" or "ring of fractions").

[lmm]

It's true up to NaNs, which we can treat as bottoms.