[Agda] question on `compare'

[Sergei Meshveliani]

Please, what is wrong here?

--------------------------------------------------------------------
open import Function        using (case_of_)
open import Relation.Binary using (module DecTotalOrder;
                                   module StrictTotalOrder; module Tri)
open import Data.Empty using (⊥-elim)
open import Data.Nat as Nat using (ℕ; _≮_; _≤_; _≥_; _<_)
open import Data.Nat.Properties as NatProp using ()

open StrictTotalOrder NatProp.strictTotalOrder using (compare)
open DecTotalOrder    Nat.decTotalOrder using () 
                                        renaming (reflexive to ≤refl)
open Tri


postulate  <→≤ : ∀ {m n} → m < n → m ≤ n

≮→≥ : ∀ {m n} → m ≮ n → n ≤ m
≮→≥ {m} {n} m≮n =
    case compare m n
    of \
    { (tri< m<n _   _   ) → ⊥-elim (m≮n m<n)
    ; (tri≈ _   m=n _   ) → ≤refl m=n
    ; (tri> _   _    m>n) → let n<m : n < m
        		        n<m = m>n

        		        n≤m : n ≤ m
        		        n≤m = <→≤ {n} {m} n<m
                            in
        		    n≤m
    }
---------------------------------------------------------------

" n != m of type ℕ
  when checking that the expression n≤m has type m ≤ n
"

The signature for ≮→≥  ends with  m ≤ n. 

So, why does  Agda 2.4.2.2  expect  m ≤ n
?

Thanks,

------
Sergei