How to define list of natural numbers without gaps in Coq?
For example [2, 1, 3] is valid list, but [5, 1, 3] is not because it have two gaps: between 1 and 3, 3 and 5.
I have try to ask Google, but nothing similar was found
You could say that a list of length n is without gaps iff its sorted version is equal to the list of naturals from 1 to n. If need be, this could be packaged in a dependent record, with the list and its no-gap property as fields.