Невозможно доказать, что только 0 меньше 1 с помощью finTypes mathcomp

Question

Этот вопрос может показаться очень глупым, но я не могу доказать, что единственное натуральное число меньше 1 - 0. Я использую библиотеку mathcomp finType, и цель, которую я хочу доказать:

Lemma ord0_eq1 (a : ordinal 1) : a = ord0.

Проблема в том, что если я уничтожу a и ord0, я получу следующую цель:

∀ (m : nat) (i : (m < 1)%N), Ordinal i = Ordinal (ltn0Sn 0)

Теперь я могу использовать case и получить абсурд, если m не равно 0. Но если m равно 0, я получаю:

∀ i : (0 < 1)%N, Ordinal i = Ordinal (ltn0Sn 0)

И единственный способ доказать это равенство - доказать, что forall i : 0 < 1, i = (ltn0Sn 0). Но я не знаю, как доказать равенство между двумя доказательствами одного и того же Prop без использования ненужных доказательств, и я не хочу добавлять аксиому в мою теорию. Должен быть какой-то способ использовать возможности отражения Ssreflect для решения этой цели, но я ничего не нашел: я могу добраться до точки, где мне нужно доказать равенство между двумя доказательствами равенства, и я мог бы использовать UIP (уникальность доказательства личности), но это еще одна аксиома, и я не хочу ее использовать.

Я не могу поверить, что мне нужно добавить аксиому, чтобы доказать эту цель: отношение меньше чем может быть определено только вычислением. Должен быть способ доказать, что forall (m n : nat) (a b : m < n), a = b без UIP или доказательства несоответствия.

Спасибо

EDIT : я использую библиотеку ssrnat mathcomp, а не Coq * Модуль 1025 *. Запись "<" связана с ltn от ssrnat, а не lt от Arith.

Answer 1

Предикат, определяющий тип ordinal, является булевым равенством, следовательно, удовлетворяет несоответствию доказательства. В таких случаях вы можете обратиться к val_inj:

From mathcomp Require Import all_ssreflect.

Lemma ord0_eq1 (a : ordinal 1) : a = ord0.
Proof. by apply/val_inj; case: (val a) (valP a). Qed.