How to construct a data type with specified properties?

Question

Functional programming

It is necessary to construct a data type in some functional language.
This data type must contain a parameter - the number of its elements.
These elements should be different accordingly.
They must be linearly ordered, there must be a smallest and a largest element.
On this data type, functions will be built to move to the next and previous element, access to the smallest and largest element.
In general, so to speak, a list of numbers or an alphabet.
On Coq I built the following data type:
Definition SS n := {m : nat | m<n}.
Those. like a set of natural numbers less than a given n.
The problem is that proving that this or that natural number is included in this set portends a comparison of numbers, which is terribly cumbersome, and it cannot even be generalized to any number.
Here is an example proof that 0 is in this set:
OelSS10 =
exist (fun m : nat => m < 10) 0
(le_S 1 9
(le_S 1 8
(le_S 1 7
(le_S 1 6
(le_S 1 5
(le_S 1 4
(le_S 1 3
(le_S 1 2
(le_S 1 1 (le_n 1))))))))))
: SS 10
You can of course just set the type manually Iductive SS := c0 | c1 | c2 | c3 | c4.
But here at least there is no orderliness, and manually you will be tired of describing it.
Please help, I've been struggling with this problem for a long time.

Answer 1

One forum suggested such an option for describing a finite set.
Inductive Fin : nat -> Type :=
| FZ : forall k:nat, Fin(Sk)
| FS : forall k:nat, Fink -> Fin(Sk).
(On Idris https://github.com/idris-lang/Idris-dev/blob/maste... )
I changed this type and got this
Inductive Fin : nat -> Type :=
| FZ : Fin 0
| FS : forall k:nat, Fink -> Fin(Sk).
Using this type, you can specify either an empty set or a set of a finite number of elements.
PS: I created a group about Coq , I post translations of the chapters of the official reference manual, I write what I noticed interesting. I would be happy to discuss various issues.