```
a =? a - 1 = false.
```

To prove this i have to put condition on a because natural number start from a (otherwise i will get 0=-1)

Hi @pianke , a bit of context is missing from your question, but indeed if `a`

is of type `nat`

, there is a problem when a = 0

Note that often `0 - 1`

is defined in Coq to be 0

Last updated: Jun 18 2024 at 20:02 UTC