[Agda] ℕ <--iso--> Bin⁺ ∩ HasLast1if

[Sergei Meshveliani]

People, 

as an exercise in Agda, I provide 

   http://botik.ru/pub/local/Mechveliani/agdaNotes/bin2.zip

-- my own proof in Agda for  suc - isomorphism between  ℕ  and its
binary codes
-- an addition to  Standard library lib-0.7.


1. It uses the binary code (Bin⁺) representation in which

   0 <--> [],  and a binary code either is  []  or ends with  1b
                                            (as the higher bit).
This higher bit condition is expressed as  HasLast1if, HasLast1.

2. It is proved in  Bin.agda  that
                    ℕ  <--suc-isomorphic-->  Bin⁺ ∩ HasLast1if,
   where
         suc  corresponds to  addCarryToBitList.

3. For this aim, we re-implement   toDigits   in the form of

   toBDigits : (n : ℕ) → ∃ \ (bs : Bin⁺) →
                             fromDigits bs ≡ n × HasLast1if bs
(for  base = 2  only)
- because it is easier for us to compose proofs for such.

4. The main parts are
   toBDigits,
   injective-fromDigits
           - injectiveness of  fromDigits  on  Bin⁺ ∩ HasLast1if.

5. My question is:
   can this be proved in a simpler/shorter (nicer) way?
   (for example,  injective-fromDigits  looks lengthy). 

6. The program consists of the two modules and is tested under

   Agda-2.3.3-pre Malonzo, lib-0.7
   - both of the development version of  November 24, 2013.

(the 2.3.2.2 version, or lower ones, will not do).

I hope it will also work under any later version.

Regards,

------
Sergei