[Agda] _<_ of agda-prelude

[Sergei Meshveliani]

Can anybody, please, show a proof for equivalence of standard _<_ and
the one of agda-prelude?
I am stuck with the code

<'→< :  ∀ m n → Ord._<_ OrdNat m n → m < n
                                                              
<'→< 0 (suc _) _ =  s≤s z≤n
<'→< _ 0       _ =  
                 ?                                                 

≮'0 :  ∀ n → ¬ (Ord._<_ OrdNat n 0)                        
≮'0 n n<'0 = 
           ?   

Thanks,

------
Sergei