`Bin : Type`

Bin represents binary numbers right-to-left.

For instance `4` can be represented as `OOI`.

Note that representations are not unique: one may append arbitrarily

many Os to the right of the representation without changing the meaning.

**Totality**: total

**Visibility**: public export`toNat : Bin -> Nat`

Conversion from lists of bits to natural number.

**Totality**: total

**Visibility**: public export`suc : Bin -> Bin`

Successor function on binary numbers.

Amortised constant time.

**Totality**: total

**Visibility**: public export`sucCorrect : toNat (suc bs) = S (toNat bs)`

Correctness proof of `suc` with respect to the semantics in terms of Nat

**Totality**: total

**Visibility**: export