[Agda] fastCompare for Nat

[Sergei Meshveliani]

Dear standard library developers,

The comparison  Nat.<-cmp  is `exponentially' slow.

As lib-0.18-candidate  has fast  _≡ᵇ_ and _<ᵇ_, 
and as _≟_ is also fast on Nat (when the proof is not inspected),
this gives a hope for making <-cmp fast in a similar sense.

The below  compareFast  implements the goal by using that _∸_ is
expressed via built-in.

I wonder of whether standard library supports a simpler solution. 
If it does not, then maybe it could incorporate a similar thing. 

Thanks,

------
Sergei


--------------------------------------------------------------
compareFast :  (m n : ℕ) → Tri (m < n) (m ≡ n) (m > n)
--
-- _≟_ and _∸_ are via built-in.

compareFast m n =  aux (m ≟ n) (m ∸ n) (n ∸ m) refl refl 
  where
  aux :  Dec (m ≡ n) → (d d' : ℕ) → m ∸ n ≡ d → n ∸ m ≡ d' →
                               Tri (m < n) (m ≡ n) (m > n)

  aux (yes m≡n) _ _ _ _ =  tri≈ (<-irrefl m≡n) m≡n m≯n
                           where
                           m≯n = <-irrefl (sym m≡n)

  aux (no m≢n) 0 _ m∸n≡0 _ =  tri< m<n m≢n (<-asym m<n) 
                              where
                              m≤n =  m∸n≡0⇒m≤n m∸n≡0
                              m<n =  ≤,≢⇒< m≤n m≢n

  aux (no m≢n) (suc _) 0 _ n∸m≡0 =  
                           tri> (<-asym n<m) m≢n n<m
                           where
                           n≤m  =  m∸n≡0⇒m≤n n∸m≡0
                           n≢m =  m≢n ∘ sym
                           n<m  =  ≤,≢⇒< n≤m n≢m

  aux _ (suc d₁) (suc d₂) m∸n≡1+d₁ n∸m≡1+d₂ =  
                          contradiction n<m (<-asym m<n)
      where
      m∸n≢0 = \m-n≡0 → let 1+d₁≡0 = trans (sym m∸n≡1+d₁) m-n≡0
                       in  suc≢0 1+d₁≡0

      n∸m≢0 = \n-m≡0 → let 1+d₂≡0 = trans (sym n∸m≡1+d₂) n-m≡0
                       in  suc≢0 1+d₂≡0

      n<m = m∸n≢0⇒n<m {m} {n} m∸n≢0
      m<n = m∸n≢0⇒n<m n∸m≢0