[Agda] Re: Nat -iso- Bin

[Sergei Meshveliani]

To my request on Bin -- Nat isomorphism
Arseniy Alekseyev  wrote

> FWIW, there is my proof of bijection together with proofs of
> equivalence for addition and multiplication:
> https://github.com/Rotsor/BinDivMod
> See modules Data.Bin.{Bijection, Addition, Multiplication}
> Too bloated, I guess, but that's what I've got.

Thank you. I have downloaded it, for a reserve.

lib-0.7  already has _+_ and _*_ for Bin.
Do you redefine them in  Addition, Multiplication ?

Thanks,

------
Sergei