Implement ≤-total in terms of _≤?_

CHANGELOG.md

@@ -15,6 +15,11 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The implementation of `≤-total` in `Data.Nat.Properties` has been altered
+ to use operations backed by primitives, rather than recursion, making it
+ significantly faster. However, its reduction behaviour on open terms may have
+ changed.
+
 Minor improvements
 ------------------
 

src/Data/Nat/Properties.agda

@@ -162,6 +162,11 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 -- Properties of _≤_
 ------------------------------------------------------------------------
 
+≰⇒≥ : _≰_ ⇒ _≥_
+≰⇒≥ {m} {zero} m≰n = z≤n
+≰⇒≥ {zero} {suc n} m≰n = contradiction z≤n m≰n
+≰⇒≥ {suc m} {suc n} m≰n = s≤s (≰⇒≥ (m≰n ∘ s≤s))
+
 ------------------------------------------------------------------------
 -- Relational properties of _≤_
 
@@ -180,11 +185,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤-trans z≤n _ = z≤n
 ≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)
 
-≤-total : Total _≤_
-≤-total zero _ = inj₁ z≤n
-≤-total _ zero = inj₂ z≤n
-≤-total (suc m) (suc n) = Sum.map s≤s s≤s (≤-total m n)
-
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant z≤n z≤n = refl
 ≤-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevant m≤n₁ m≤n₂)
@@ -203,6 +203,11 @@ m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n))
 _≥?_ : Decidable _≥_
 _≥?_ = flip _≤?_
 
+≤-total : Total _≤_
+≤-total m n with m ≤? n
+... | yes m≤n = inj₁ m≤n
+... | no m≰n = inj₂ (≰⇒≥ m≰n)
+
 ------------------------------------------------------------------------
 -- Structures
 
@@ -331,9 +336,6 @@ n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl
 ≰⇒> {suc m} {zero} _ = z<s
 ≰⇒> {suc m} {suc n} m≰n = s<s (≰⇒> (m≰n ∘ s≤s))
 
-≰⇒≥ : _≰_ ⇒ _≥_
-≰⇒≥ = <⇒≤ ∘ ≰⇒>
-
 ≮⇒≥ : _≮_ ⇒ _≥_
 ≮⇒≥ {_} {zero} _ = z≤n
 ≮⇒≥ {zero} {suc j} 1≮j+1 = contradiction z<s 1≮j+1