An alternative to #1698

src/Data/Fin/Base.agda

@@ -13,8 +13,7 @@
 module Data.Fin.Base where
 
 open import Data.Empty using (⊥-elim)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; _^_)
-open import Data.Nat.Properties.Core using (≤-pred)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
@@ -67,8 +66,8 @@ fromℕ (suc n) = suc (fromℕ n)
 -- fromℕ< {m} _ = "m".
 
 fromℕ< : ∀ {m n} → m ℕ.< n → Fin n
-fromℕ< {zero}  {suc n} m≤n = zero
-fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (≤-pred m≤n))
+fromℕ< {zero}  {suc n} z<s = zero
+fromℕ< {suc m} {suc n} (s<s m<n@(s≤s _)) = suc (fromℕ< m<n)
 
 -- fromℕ<″ m _ = "m".
 
@@ -112,8 +111,8 @@ inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
 inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
-inject≤ {_} {suc n} zero    le = zero
-inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (≤-pred le))
+inject≤ {_} {suc n} zero    _        = zero
+inject≤ {_} {suc n} (suc i) (s≤s le) = suc (inject≤ i le)
 
 -- lower₁ "i" _ = "i".
 

src/Data/Fin/Induction.agda

@@ -8,7 +8,7 @@
 
 open import Data.Fin.Base
 open import Data.Fin.Properties
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; _∸_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_)
 import Data.Nat.Induction as ℕ
 import Data.Nat.Properties as ℕ
 open import Induction
@@ -46,15 +46,15 @@ open WF public using (Acc; acc)
   induct : ∀ {i} → Acc _<_ i → P i
   induct {zero}  _         = P₀
   induct {suc i} (acc rec) = Pᵢ⇒Pᵢ₊₁ i (induct (rec (inject₁ i) i<i+1))
-    where i<i+1 = s≤s (ℕ.≤-reflexive (toℕ-inject₁ i))
+    where i<i+1 = ℕ<⇒inject₁< (ℕ.n<1+n (toℕ i))
 
 ------------------------------------------------------------------------
 -- Induction over _>_
 
 private
   acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
-  acc-map {n} (acc rs) = acc (λ y y>x →
-    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y))))
+  acc-map {n} (acc rs) = acc λ y y>x →
+    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -69,7 +69,7 @@ private
   induct {i} (acc rec) with n ℕ.≟ toℕ i
   ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
-    where Pᵢ₊₁ = induct (rec _ (s≤s (ℕ.≤-reflexive (sym (toℕ-lower₁ i n≢i)))))
+    where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Induction over _≺_

src/Data/Fin/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
@@ -135,12 +135,19 @@ toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 ↑ʳ-injective zero i i refl = refl
 ↑ʳ-injective (suc n) i j eq = ↑ʳ-injective n i j (suc-injective eq)
 
+------------------------------------------------------------------------
+-- toℕ and the ordering relations
+------------------------------------------------------------------------
+
+new-toℕ≤n : ∀ {n} → (i : Fin (suc n)) → toℕ i ℕ.≤ n
+new-toℕ≤n {_}     zero    = z≤n
+new-toℕ≤n {suc n} (suc i) = s≤s (new-toℕ≤n i)
+
 toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ.< n
-toℕ<n zero    = s≤s z≤n
-toℕ<n (suc i) = s≤s (toℕ<n i)
+toℕ<n {suc n} i = s≤s (new-toℕ≤n i)
 
 toℕ≤n : ∀ {n} → (i : Fin n) → toℕ i ℕ.≤ n
-toℕ≤n = ℕₚ.<⇒≤ ∘ toℕ<n
+toℕ≤n {suc n} i = ℕₚ.≤-step (new-toℕ≤n i)
 
 toℕ≤pred[n] : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n] zero                 = z≤n
@@ -154,20 +161,20 @@ toℕ≤pred[n]′ : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n]′ i = ℕₚ.<⇒≤pred (toℕ<n i)
 
 toℕ-mono-< : ∀ {n} {i j : Fin n} → i < j → toℕ i ℕ.< toℕ j
-toℕ-mono-< {i = 0F}    {suc j}       (s≤s z≤n)       = s≤s z≤n
-toℕ-mono-< {i = suc i} {suc (suc j)} (s≤s (s≤s i<j)) = s≤s (toℕ-mono-< (s≤s i<j))
+toℕ-mono-< {i = 0F}    {suc j}       z<s               = z<s
+toℕ-mono-< {i = suc i} {suc (suc j)} (s<s i<j@(s≤s _)) = s<s (toℕ-mono-< i<j)
 
 toℕ-mono-≤ : ∀ {n} {i j : Fin n} → i ≤ j → toℕ i ℕ.≤ toℕ j
-toℕ-mono-≤ {i = 0F} {j} z≤n = z≤n
+toℕ-mono-≤ {i = 0F}    {j}     z≤n       = z≤n
 toℕ-mono-≤ {i = suc i} {suc j} (s≤s i≤j) = s≤s (toℕ-mono-≤ i≤j)
 
 toℕ-cancel-≤ : ∀ {n} {i j : Fin n} → toℕ i ℕ.≤ toℕ j → i ≤ j
-toℕ-cancel-≤ {i = 0F} {j} z≤n = z≤n
+toℕ-cancel-≤ {i = 0F}    {j}     z≤n       = z≤n
 toℕ-cancel-≤ {i = suc i} {suc j} (s≤s i≤j) = s≤s (toℕ-cancel-≤ i≤j)
 
 toℕ-cancel-< : ∀ {n} {i j : Fin n} → toℕ i ℕ.< toℕ j → i < j
-toℕ-cancel-< {i = 0F} {suc j} (s≤s z≤n) = s≤s z≤n
-toℕ-cancel-< {i = suc i} {suc (suc j)} (s≤s (s≤s i<j)) = s≤s (toℕ-cancel-< (s≤s i<j))
+toℕ-cancel-< {i = 0F}    {suc j}       z<s               = z<s
+toℕ-cancel-< {i = suc i} {suc (suc j)} (s<s i<j@(s≤s _)) = s<s (toℕ-cancel-< i<j)
 
 ------------------------------------------------------------------------
 -- fromℕ
@@ -182,19 +189,19 @@ fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
 ≤fromℕ : ∀ {n} → (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
-≤fromℕ {n} i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ n)) (ℕₚ.≤-pred (toℕ<n i))
+≤fromℕ {n} i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ n)) (new-toℕ≤n i)
 
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
 fromℕ<-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ.< m) → fromℕ< i<m ≡ i
-fromℕ<-toℕ zero    (s≤s z≤n)       = refl
-fromℕ<-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ<-toℕ i (s≤s m≤n))
+fromℕ<-toℕ zero    z<s               = refl
+fromℕ<-toℕ (suc i) (s<s m<n@(s≤s _)) = cong suc (fromℕ<-toℕ i m<n)
 
 toℕ-fromℕ< : ∀ {m n} (m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< (s≤s z≤n)       = refl
-toℕ-fromℕ< (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ< (s≤s m<n))
+toℕ-fromℕ< z<s               = refl
+toℕ-fromℕ< (s<s m<n@(s≤s _)) = cong suc (toℕ-fromℕ< m<n)
 
 -- fromℕ is a special case of fromℕ<.
 fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
@@ -205,28 +212,28 @@ fromℕ<-cong : ∀ m n {o} → m ≡ n →
               (m<o : m ℕ.< o) →
               (n<o : n ℕ.< o) →
               fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-cong 0       0       r (s≤s z≤n)     (s≤s z≤n)     = refl
-fromℕ<-cong (suc _) (suc _) r (s≤s (s≤s p)) (s≤s (s≤s q))
-  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) (s≤s p) (s≤s q))
+fromℕ<-cong 0       0       r z<s               z<s  = refl
+fromℕ<-cong (suc _) (suc _) r (s<s m<n@(s≤s _)) (s<s n<o@(s≤s _))
+  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) m<n n<o)
 
 fromℕ<-injective : ∀ m n {o} →
                    (m<o : m ℕ.< o) →
                    (n<o : n ℕ.< o) →
                    fromℕ< m<o ≡ fromℕ< n<o →
                    m ≡ n
-fromℕ<-injective 0 0 (s≤s z≤n) (s≤s z≤n) r = refl
-fromℕ<-injective (suc _) (suc _) (s≤s (s≤s p)) (s≤s (s≤s q)) r
-  = cong suc (fromℕ<-injective _ _ (s≤s p) (s≤s q) (suc-injective r))
+fromℕ<-injective 0       0       z<s               z<s r = refl
+fromℕ<-injective (suc _) (suc _) (s<s m<n@(s≤s _)) (s<s n<o@(s≤s _)) r
+  = cong suc (fromℕ<-injective _ _ m<n n<o (suc-injective r))
 
 ------------------------------------------------------------------------
 -- fromℕ<″
 ------------------------------------------------------------------------
 
 fromℕ<≡fromℕ<″ : ∀ {m n} (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ (s≤s z≤n)       (ℕ.less-than-or-equal refl) = refl
-fromℕ<≡fromℕ<″ (s≤s (s≤s m<n)) (ℕ.less-than-or-equal refl) =
-  cong suc (fromℕ<≡fromℕ<″ (s≤s m<n) (ℕ.less-than-or-equal refl))
+fromℕ<≡fromℕ<″ z<s               (ℕ.less-than-or-equal refl) = refl
+fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.less-than-or-equal refl) =
+  cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.less-than-or-equal refl))
 
 toℕ-fromℕ<″ : ∀ {m n} (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<n = begin
@@ -341,12 +348,12 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 <-trans = ℕₚ.<-trans
 
 <-cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
-<-cmp zero    zero    = tri≈ (λ())     refl  (λ())
-<-cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
-<-cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
+<-cmp zero    zero    = tri≈ (λ()) refl  (λ())
+<-cmp zero    (suc j) = tri< z<s   (λ()) (λ())
+<-cmp (suc i) zero    = tri> (λ()) (λ()) z<s
 <-cmp (suc i) (suc j) with <-cmp i j
-... | tri< i<j i≢j j≮i = tri< (s≤s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
-... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s≤s j<i)
+... | tri< i<j i≢j j≮i = tri< (s<s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
+... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s<s j<i)
 ... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
 
 <-respˡ-≡ : ∀ {m n} → (_<_ {m} {n}) Respectsˡ _≡_
@@ -400,9 +407,9 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 
 ≤∧≢⇒< : ∀ {n} {i j : Fin n} → i ≤ j → i ≢ j → i < j
 ≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
-≤∧≢⇒< {i = zero}  {suc j} _         _       = s≤s z≤n
+≤∧≢⇒< {i = zero}  {suc j} _         _       = z<s
 ≤∧≢⇒< {i = suc i} {suc j} (s≤s i≤j) 1+i≢1+j =
-  s≤s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))
+  s<s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))
 
 ------------------------------------------------------------------------
 -- inject
@@ -436,7 +443,7 @@ inject₁ℕ≤ : ∀ {n} → (i : Fin n) → toℕ (inject₁ i) ℕ.≤ n
 inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 
 ≤̄⇒inject₁< : ∀ {n} → {i j : Fin n} → j ≤ i → inject₁ j < suc i
-≤̄⇒inject₁< {i = i} {j} p = subst (ℕ._< toℕ (suc i)) (sym (toℕ-inject₁ j)) (s≤s p)
+≤̄⇒inject₁< {i = i} {j} p = subst (ℕ._< toℕ (suc i)) (sym (toℕ-inject₁ j)) (s<s p)
 
 ℕ<⇒inject₁< : ∀ {n} → {i : Fin (ℕ.suc n)} → {j : Fin n} →
               toℕ j ℕ.< toℕ i → inject₁ j < i
@@ -492,18 +499,18 @@ inject₁≡⇒lower₁≡ ≢p ≡p = inject₁-injective (trans (inject₁-low
 toℕ-inject≤ : ∀ {m n} (i : Fin m) (le : m ℕ.≤ n) →
                 toℕ (inject≤ i le) ≡ toℕ i
 toℕ-inject≤ {_} {suc n} zero    _  = refl
-toℕ-inject≤ {_} {suc n} (suc i) le = cong suc (toℕ-inject≤ i (ℕₚ.≤-pred le))
+toℕ-inject≤ {_} {suc n} (suc i) (s≤s le) = cong suc (toℕ-inject≤ i le)
 
 inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
 inject≤-refl {suc n} zero    _   = refl
-inject≤-refl {suc n} (suc i) n≤n = cong suc (inject≤-refl i (ℕₚ.≤-pred n≤n))
+inject≤-refl {suc n} (suc i) (s≤s n≤n) = cong suc (inject≤-refl i n≤n)
 
 inject≤-idempotent : ∀ {m n k} (i : Fin m)
                      (m≤n : m ℕ.≤ n) (n≤k : n ℕ.≤ k) (m≤k : m ℕ.≤ k) →
                      inject≤ (inject≤ i m≤n) n≤k ≡ inject≤ i m≤k
 inject≤-idempotent {_} {suc n} {suc k} zero    _   _   _ = refl
-inject≤-idempotent {_} {suc n} {suc k} (suc i) m≤n n≤k _ =
-  cong suc (inject≤-idempotent i (ℕₚ.≤-pred m≤n) (ℕₚ.≤-pred n≤k) _)
+inject≤-idempotent {_} {suc n} {suc k} (suc i) (s≤s m≤n) (s≤s n≤k) (s≤s m≤k) =
+  cong suc (inject≤-idempotent i m≤n n≤k m≤k)
 
 inject≤-injective : ∀ {n m} (n≤m n≤m′ : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
 inject≤-injective (s≤s p) (s≤s q) zero zero eq = refl
@@ -549,8 +556,8 @@ join-splitAt (suc m) n (suc i) = begin
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
 splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
-splitAt-< (suc m) zero    _         = refl
-splitAt-< (suc m) (suc i) (s≤s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
+splitAt-< (suc m) zero    z<s               = refl
+splitAt-< (suc m) (suc i) (s<s i<m@(s≤s _)) = cong (Sum.map suc id) (splitAt-< m i i<m)
 
 -- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
 
@@ -752,8 +759,8 @@ lift-injective f inj (suc k) {suc i} {suc y} eq = cong suc (lift-injective f inj
 ------------------------------------------------------------------------
 
 <⇒≤pred : ∀ {n} {i j : Fin n} → j < i → j ≤ pred i
-<⇒≤pred {i = suc i} {zero}  j<i       = z≤n
-<⇒≤pred {i = suc i} {suc j} (s≤s j<i) =
+<⇒≤pred {i = suc i} {zero}  z<s       = z≤n
+<⇒≤pred {i = suc i} {suc j} (s<s j<i) =
   subst (_ ℕ.≤_) (sym (toℕ-inject₁ i)) j<i
 
 ------------------------------------------------------------------------
@@ -934,10 +941,10 @@ private
 
 pigeonhole : ∀ {m n} → m ℕ.< n → (f : Fin n → Fin m) →
              ∃₂ λ i j → i ≢ j × f i ≡ f j
-pigeonhole (s≤s z≤n)       f = contradiction (f zero) λ()
-pigeonhole (s≤s (s≤s m≤n)) f with any? (λ k → f zero ≟ f (suc k))
+pigeonhole z<s       f = contradiction (f zero) λ()
+pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , (λ()) , f₀≡fⱼ
-... | no  f₀≢fₖ with pigeonhole (s≤s m≤n) (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+... | no  f₀≢fₖ with pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
 ...   | (i , j , i≢j , fᵢ≡fⱼ) =
   suc i , suc j , i≢j ∘ suc-injective ,
   punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
@@ -988,7 +995,7 @@ opposite-involutive : ∀ {n} → Involutive {A = Fin n} _≡_ opposite
 opposite-involutive {suc n} i = toℕ-injective (begin
   toℕ (opposite (opposite i)) ≡⟨ opposite-prop (opposite i) ⟩
   n ∸ (toℕ (opposite i))     ≡⟨ cong (n ∸_) (opposite-prop i) ⟩
-  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (ℕₚ.≤-pred (toℕ<n i)) ⟩
+  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (new-toℕ≤n i) ⟩
   toℕ i                     ∎)
   where open ≡-Reasoning
 
@@ -1083,7 +1090,6 @@ Please use join-splitAt instead."
 #-}
 
 -- Version 2.0
-
 toℕ-raise = toℕ-↑ʳ
 {-# WARNING_ON_USAGE toℕ-raise
 "Warning: toℕ-raise was deprecated in v2.0.

src/Data/Nat/Base.agda

@@ -55,6 +55,15 @@ data _≤_ : Rel ℕ 0ℓ where
 _<_ : Rel ℕ 0ℓ
 m < n = suc m ≤ n
 
+------------------------------------------------------------------------
+-- Smart constructors of _<_
+
+pattern z<s {n}         = s≤s (z≤n {n})
+pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+
+------------------------------------------------------------------------
+-- other ordering relations
+
 _≥_ : Rel ℕ 0ℓ
 m ≥ n = n ≤ m
 
@@ -101,15 +110,15 @@ instance
 ≢-nonZero {suc n} n≢0 = _
 
 >-nonZero : ∀ {n} → n > 0 → NonZero n
->-nonZero (s≤s 0<n) = _
+>-nonZero z<s = _
 
 -- Destructors
 
 ≢-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n ≢ 0
 ≢-nonZero⁻¹ (suc n) ()
 
 >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
->-nonZero⁻¹ (suc n) = s≤s z≤n
+>-nonZero⁻¹ (suc n) = z<s
 
 ------------------------------------------------------------------------
 -- Arithmetic
@@ -183,6 +192,12 @@ data _≤′_ (m : ℕ) : ℕ → Set where
 _<′_ : Rel ℕ 0ℓ
 m <′ n = suc m ≤′ n
 
+------------------------------------------------------------------------
+-- Smart constructors of _<′_
+
+pattern n<′1+n           = ≤′-refl
+pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+
 _≥′_ : Rel ℕ 0ℓ
 m ≥′ n = n ≤′ m
 

src/Data/Nat/Induction.agda

@@ -9,12 +9,13 @@
 module Data.Nat.Induction where
 
 open import Function
-open import Data.Nat.Base
-open import Data.Nat.Properties using (≤⇒≤′; n<1+n)
+open import Data.Nat.Base using (ℕ; zero; suc; _<_; _<′_; n<′1+n; <′-step)
+open import Data.Nat.Properties using (m<1+n⇒m<n∨m≡n)
 open import Data.Product
+open import Data.Sum using (inj₁; inj₂)
 open import Data.Unit.Polymorphic
 open import Induction
-open import Induction.WellFounded as WF
+open import Induction.WellFounded as WF using (WellFounded; WfRec)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary
@@ -69,8 +70,8 @@ mutual
   <′-wellFounded n = acc (<′-wellFounded′ n)
 
   <′-wellFounded′ : ∀ n → <′-Rec (Acc _<′_) n
-  <′-wellFounded′ (suc n) .n ≤′-refl       = <′-wellFounded n
-  <′-wellFounded′ (suc n)  m (≤′-step m<n) = <′-wellFounded′ n m m<n
+  <′-wellFounded′ (suc n) .n n<′1+n        = <′-wellFounded n
+  <′-wellFounded′ (suc n)  m (<′-step m<n) = <′-wellFounded′ n m m<n
 
 module _ {ℓ} where
   open WF.All <′-wellFounded ℓ public
@@ -85,8 +86,16 @@ module _ {ℓ} where
 <-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
 <-Rec = WfRec _<_
 
-<-wellFounded : WellFounded _<_
-<-wellFounded = Subrelation.wellFounded ≤⇒≤′ <′-wellFounded
+mutual
+
+  <-wellFounded : WellFounded _<_
+  <-wellFounded n = acc (<-wellFounded′ n)
+
+  <-wellFounded′ : ∀ n → <-Rec (Acc _<_) n
+  <-wellFounded′ zero    y ()
+  <-wellFounded′ (suc n) y y<1+n with <-wellFounded n | m<1+n⇒m<n∨m≡n y<1+n
+  ... | wfn@(acc rec) | inj₁ y<n  = rec y y<n
+  ... | wfn           | inj₂ refl = wfn
 
 -- A version of `<-wellFounded` that cheats by skipping building
 -- the first billion proofs. Use this when you require the function