[Agda] Q: Equational Reasoning

[ch]

Hi,

I am new to Agda and confused by all the library modules.

Is there an easy way to make the properties of the
operations on built-in natural numbers available for equational
reasoning without copying larger parts of library code
(especially those in private sections) into own Agda scripts
and without a tedious top-down refinement of the algebraic
definitions?

Basically, I would like something like this:

    begin
      ...
      m * n
      =< Data.Nat.\nb.commutativity-* {m} {n} >
      n * m
      ...

Could you please tell me, what has to be written inside the  =< ... >  
brackets
to achieve that? And what is the preferred library module to use for
equational reasoning (=,  not <=) on the built-in Data.Nat.\nb type?

If there is a specific tutorial on how to do equational reasoning in 
Agda or on the
concept of how to deal with the libraries (when to use using, hiding, 
renaming),
please give me the pointer.

Many thanks in advance
--
 Christoph