[Agda] `accessible' for ℕ

[Sergei Meshveliani]

This is on Standard library. 

Please, how to extract
               <-acc : {n : ℕ} →Acc _<_

from  Induction.Nat ?

I program it by

  <-acc {0}      =  acc (\_ ())
  <-acc {suc n}  with <-acc {n}
  ...            | acc wf = acc f
                            where ...,

but probably it can be somehow imported from Induction.Nat.

Thanks,

------
Sergei