[Agda] Nat -iso- Bin

[Sergei Meshveliani]

Please, has  lib-0.7  something for the isomorphism  ℕ <-> Bin ?

For example, I need 

  toDigits-suc-eq : {m : ℕ} → 
                    let toDs : ℕ → Bin⁺
                        toDs = proj₁ ∘ toDigits 2                    
                    in 
                    toDs ∘ suc ≗ (addCarryToBitList 1b ∘ toDs) 

Probably,      fromℕ ∘ suc ≗ Bin.suc ∘ fromℕ 
will also do.

I think of proving  toDigits-suc-eq,  but this needs looking into a
non-trivial definition of  toDigits.

Thanks,

------
Sergei