EECS 755

Software Requirements Modeling and Analysis



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.