Implement ≤-total in terms of _≤?_ (#2440)

* Define Data.Nat.≰⇒≥ directly and earlier

* Define Data.Nat.≤-total in terms of _≤?_

* Update changelog

* Be a bit lazier

Author: Taneb

CHANGELOG.md

@@ -12,6 +12,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
+... | true because m≤n = inj₁ (invert m≤n)
+... | false because m≰n = inj₂ (≰⇒≥ (invert 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