Сопоставление с шаблоном, не специализирующееся на типах

Я играю в Coq, пытаюсь создать отсортированный список. Мне просто нужна функция, которая принимает список [1,2,3,2,4] и возвращает что-то вроде Sorted [1,2,3,4] - т.е. исключить плохие части, но не сортировать весь список.

Я подумал, что начну с определения функции lesseq типа (mn: nat) -> option (m <= n ) , и тогда я мог довольно легко найти сопоставление с образцом. Возможно, это плохая идея.

Суть проблемы, с которой я столкнулся сейчас, заключается в том, что (сниппет, вся функция внизу)

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
        | 0 => match n with
            | 0 => Some (le_n 0)
            ...

не проверяет типы; он говорит, что ожидает вариант (m <= n) , но что Some (le_n 0) имеет вариант типа (0 <= 0) . Я не понимаю, потому что, очевидно, и m , и n в этом контексте равны нулю, но я ' Я понятия не имею, как сказать Coq об этом.

Вся функция такова:

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
    | 0 => match n with
        | 0 => Some (le_n 0)
        | S n_  => None
        end
    | S m_  => match n with
        | 0 => None
        | S _   => match lesseq m_ n with
                | Some x=> le_S m n x
                | None  => None
                end
            end
    end.

Возможно, я забегаю вперед, и мне просто нужно продолжить чтение, прежде чем я займусь этим.