[Agda] _<_ of agda-prelude

[Jannis Limperg]

> Can anybody, please, show a proof for equivalence of standard _<_ and
> the one of agda-prelude?

Below is one proof; there are probably more elegant ones. It uses some
standard lemmas which I only redefine because I was too lazy to look up
their names.

In the future, it would be nice if you could provide a complete template
for your problem so that I don't have to muck around with the imports.

Cheers,
Jannis


----------------------------------------------------------------------


open import Data.Nat
  using (ℕ ; zero ; suc ; _+_ ; _<_ ; _≤_ ; z≤n ; s≤s)
open import Prelude.Ord using () renaming (_<_ to _<o_)
open import Prelude.Nat using (diff)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym ; trans)


≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl


≤-step : ∀ {n m} → n ≤ m → n ≤ suc m
≤-step z≤n = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)


≤-+ : ∀ n m → n ≤ m + n
≤-+ n zero = ≤-refl
≤-+ n (suc m) = ≤-step (≤-+ n m)


<o⇒< : ∀ {n m} → n <o m → n < m
<o⇒< {n} {zero} (diff k ())
<o⇒< {n} {suc m} (diff k refl) = s≤s (≤-+ n k)


+-id-right : ∀ n → n ≡ n + 0
+-id-right zero = refl
+-id-right (suc n) = cong suc (+-id-right n)


+-suc : ∀ n m → n + suc m ≡ suc (n + m)
+-suc zero m = refl
+-suc (suc n) m = cong suc (+-suc n m)


≤⇒≤o : ∀ {n m} → n ≤ m → n <o suc m
≤⇒≤o {zero} {m} z≤n = diff m (+-id-right _)
≤⇒≤o {suc n} {suc m} (s≤s n≤m) with ≤⇒≤o n≤m
... | diff k eq = diff k (cong suc (trans eq (sym (+-suc k n))))


<⇒<o : ∀ {n m} → n < m → n <o m
<⇒<o {n} {suc m} (s≤s n≤m) = ≤⇒≤o n≤m