_$_ : {A B : Set} -> (A -> B) -> A -> B
f $ x = f x
infixr 0 _$_

seven = zero

seven = suc $ suc $ suc $ suc $ suc $ suc $ suc zero

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc 5)
  ≡⟨⟩
    7
  ∎

_ : 3 * 4 ≡ 12
_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + 2 * 4
  ≡⟨⟩
    4 + 4 + 4
  ≡⟨⟩
    12
  ∎

_^_ : ℕ → ℕ → ℕ
_^_ m zero = 1
_^_ m (suc n) = m * (m ^ n)
_ : 3 ^ 4 ≡ 81
_ = refl

_ : 5 ∸ 3 ≡ 2
_ =
  begin
    5 ∸ 3
  ≡⟨⟩
    4 ∸ 2
  ≡⟨⟩
    3 ∸ 1
  ≡⟨⟩
    2 ∸ 0
  ≡⟨⟩
    2
  ∎
_ : 3 ∸ 5 ≡ 0
_ =
  begin
    3 ∸ 5
  ≡⟨⟩
    2 ∸ 4
  ≡⟨⟩
    1 ∸ 3
  ≡⟨⟩
    0 ∸ 2
  ≡⟨⟩
    0
  ∎

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
_ : inc (⟨⟩ O) ≡ ⟨⟩ I
_ = refl
_ : inc (⟨⟩ I) ≡ ⟨⟩ I O
_ = refl
_ : inc (⟨⟩ I O) ≡ ⟨⟩ I I
_ = refl
_ : inc (⟨⟩ I I) ≡ ⟨⟩ I O O
_ = refl
_ : inc (⟨⟩ I O O) ≡ ⟨⟩ I O I
_ = refl
_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl
to   : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc $ to n
_ : to 0 ≡ (⟨⟩ O)
_ = refl
_ : to 1 ≡ (⟨⟩ I)
_ = refl
_ : to 2 ≡ (⟨⟩ I O)
_ = refl
_ : to 3 ≡ (⟨⟩ I I)
_ = refl
_ : to 4 ≡ (⟨⟩ I O O)
_ = refl
_ : to 11 ≡ (⟨⟩ I O I I)
_ = refl
from : Bin → ℕ
from ⟨⟩ = 0
from (rest O) = 2 * (from rest)
from (rest I) = 1 + 2 * (from rest)
_ : from (⟨⟩ O) ≡ 0
_ = refl
_ : from (⟨⟩ I) ≡ 1
_ = refl
_ : from (⟨⟩ I O) ≡ 2
_ = refl
_ : from (⟨⟩ I I) ≡ 3
_ = refl
_ : from (⟨⟩ I O O) ≡ 4
_ = refl
_ : from (⟨⟩ I O I I) ≡ 11
_ = refl