Fix both an error by my, and a provide compatibility with older Coq versions whose `lia` is less powerful.
