Index
Blog

# Subtraction

Someone in class today asked about closure of subtraction over nat 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 nat, subtraction results that would be negative are all 0. So it goes.