Как проверить на равенство два объекта в Coq?

[zm_sansan]

Вроде элементарная операция в обычных языках программирования, но не пойму как её выполнить в Coq.
Т.е. проверить на равенство два произвольных объекта одного типа, ну например, хотя бы два натуральных числа.

Как это сделать вручную используя Check понятно.
Есть функция eq типа forall A : Type, A -> A -> Prop,
соответственно равенство строится, например так: eq nat 5 5 или eq nat 5 6, следовательно этот объект будет типа Prop.
Тип eq A x x имеет единственного обитателя, который строится конструктором eq_refl типа forall (A : Type) (x : A), eq A x x.
Например, чтобы доказать что верно eq nat 5 5 мы показываем, что он обитаем конструируя его обитателя eq_refl nat 5 типа eq nat 5 5, т.е. равенство верно. А для eq nat 5 6 мы не можем построить его обитателей, т.е. тип необитаем, значит не верно что равенство верно.
Просто выполняя Check (@eq_refl nat 5):(@eq nat 5 5), что проходит без ошибок, а Check (@eq_refl nat 5):(@eq nat 5 6) с ошибкой.

Но как это написать такую функцию для самого языка, т.е. зависимого типизированного лямбда-исчисления неясно, и как писать программы без такой элементарной операции тоже не понятно.
eq nat 5 5 не даст значения True, а просто есть какое-то значение из Prop.
Ведь обычно происходит вычисление сравниваемых объектов и сравнение их записей, и всё выдаётся true или false, в том же Хаскеле операция сравнения всегда происходила у меня без проблем.

[zm_sansan]

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

Fixpoint eq_nat a b :=
match a, b with
| O, O => true
| S a', S b' => eq_nat a' b'
| _,_ => false
end.