[Agda] Nat arithmetic properties

[Sergei Meshveliani]

Ulf Norell wrote recently

> [..]
> natural number operations (_+_, _*_ etc) are compiled to the
> corresponding Haskell Integer operations.


But this means that the properties of these operations on Nat become postulated.
Do they?

For example, the commutativity property  +-comm  of  Data.Nat.Properties.Simple
is proved in this module for Nat represented in unary system and for the algorithm for _+_ 
given in Data.Nat.
Now as _+_ is compiled to  +-via-Haskell-Integer,  the proof for +-comm  is not a proof for
+-via-Haskell-Integer.

Can somebody explain, please?

Thanks,

------
Sergei