module nat-natb where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Nat.Binary using (ℕᵇ; 1ᵇ; 1+[2_]; 2[1+_])
 renaming (zero to 0ᵇ; suc to bsuc; _+_ to _+ᵇ_)

tob : ℕ → ℕᵇ
tob = {!!}

fromb : ℕᵇ → ℕ
fromb = {!!}

fromb∘tob : ∀ (n : ℕ) → fromb (tob n) ≡ n
fromb∘tob = {!!}

tob∘fromb : ∀ (n : ℕᵇ) → tob (fromb n) ≡ n
tob∘fromb = {!!}