Построить "меньше" из stdlib "меньше"

Question

Я хотел бы преобразовать стандартную библиотеку "less" во встроенную (логическую).

Вот что у меня есть:

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat using (_<_)
open import Relation.Nullary using (Dec;yes;no)
open import Data.Nat using (ℕ;zero;suc;_<?_;z≤n;s≤s)

convert : ∀{a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
convert {_} {zero} ()
convert {zero} {suc _} _ = refl
convert {suc a} {suc b} {Data.Nat.s≤s p} eq = 
  convert {a} {b} {p} ?

Последний знак вопроса - вопрос.

Редактировать : в соответствии с предложением Галле легче доказать вспомогательную лемму. Следующий код выполняет работу:

lemma : ∀ {a b} → a Data.Nat.< b → (a < b) ≡ true
lemma {a} {zero} ()
lemma {zero} {suc b} eq = refl
lemma {suc a} {suc b} (s≤s eq) = lemma eq

convert : ∀{a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
convert {_} {zero} ()
convert {zero} {suc _} _ = refl
convert {suc a} {suc b} {Data.Nat.s≤s p} eq = lemma p

Answer 1

Легче доказать более общую лемму:

lemma : ∀ {a b} → a Data.Nat.< b → (a < b) ≡ true

А затем сделать вывод:

lemma : ∀ {a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
lemma {p = p} eq = convert p