[Agda] libraries for Bin

[Sergei Meshveliani]

Dear all,

This year I announced a library  Binary  (the current version is 3.2)
that adds certain necessary things to Standard library:              
             http://www.botik.ru/pub/local/Mechveliani/binNat/

But it looks like the same things were done by Arseniy Alekseyev in
2013:
             https://github.com/Rotsor/BinDivMod

(only the code, no `readme', no docs).
I am sorry for not looking into this attentively year ago.

Also I could, may be, save three months of effort. 
Anyway this was an exercise, the same proof functionality built in two
different ways. 

Also I look now into Coq Standard library, the part for binary natural. 
Generally, Coq shows the code, and it is difficult to find any reference
to the related papers, docs. May be, this particular subject is too
simple for a paper, but one page `readme' is desirable. 

Looking at the code, I have an impression that the Bin data is defined
there with the constructors

                            0#, double, suc-double.

`double' constructs any even number, suc-double any odd number.
I suspect that this way binary arithmetic is expressed simpler.
Only zero is not uniquely represented. But this can be fixed by
introducing four constructors instead.

Regards,

------
Sergei