Someone in class today asked about closure of subtraction over
in Coq. Actually, that wasn’t the question but it’s close enough for
jazz. I commented that
0 - 1 = 0 in Coq to a number of well-deserved
snickers. Turns out it’s true. To make subtraction closed over
subtraction results that would be negative are all
0. So it goes.