Как построить тип данных со указанными свойствами?

[zm_sansan]

Необходимо построить тип данных на некотором функциональном языке.
Это тип данных должен содержать параметр - количество его элементов.
Эти элементы соответственно должны быть различными.
Они должны быть линейно упорядочены, должен быть наименьшей и наибольший элемент.
На таком типе данных будут строиться функции для перехода к следующему и предыдущему элементу, доступу к наименьшему и наибольшему элементу.

В общем так сказать список цифр или алфавит.

На Coq я построил такой тип данных:

Definition SS n := {m : nat | m < n}.

Т.е. вроде множества из натуральных чисел меньше заданного n.
Проблема в том, что, доказательство того, что то или иное натуральное число входит в это множество, предвещает сравнение чисел, которое жутко громоздкое, и его даже не получается обобщить на любое число.

Вот например доказательство, что 0 входит в это множество:

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
Можно конечно задать просто тип вручную Iductive SS := c0 | c1 | c2 | c3 | c4.

Но тут как минимум отсутствует упорядоченность, а вручную запаришься её описывать.

Прошу помочь, долго уже бьюсь над этой проблемой.

[Portnov]

На Idris:
https://github.com/idris-lang/Idris-dev ... ta/Fin.idr
Думаю, в Coq должен быть аналог в стандартной библиотеке.

[zm_sansan]

Благодарю, то, что надо!