Contrarianism

If I told you that when n is a positive power of two and d an arbitrary number, both represented as double, the condition (n - 1) * d + d == n * d in strictly-IEEE-754-implementing C is always true, would you start looking for a counter-example, or start looking for a convincing argument that this property may hold?

If you started looking for counter-examples, would you start with the vicious values? Trying to see if NaN or +inf can be interpreted as “a positive power of two” or “an arbitrary number” represented “as double”? A subnormal value for d? A subnormal value such that n*d is normal? A subnormal value such that (n - 1) * d is subnormal and n * d is normal?

Or would you try your luck with ordinary values such as 0.1 for d and 4 for n?

This post is based on a remark by Stephen Canon. Also, I have discovered a truly remarkable proof of the property which this quick post is too small to contain.