def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two
def four : Nat = succ three
def five : Nat = succ four
def six : Nat = succ five
def seven : Nat = succ six
def eight : Nat = succ seven
def nine : Nat = succ eight
def ten : Nat = succ nine

def add : Nat -> Nat -> Nat = fun n m =>
    match n
        with zero => m
        with succ n => succ (add n m)

def mul : Nat -> Nat -> Nat = fun n m =>
    match n
        with zero => zero
        with succ n => add m (mul n m)

def pow : Nat -> Nat -> Nat = fun n m =>
    match m
        with zero => succ zero
        with succ m' => mul n (pow n m')

def sub : Nat -> Nat -> Nat = fun n m =>
    match m
        with zero => n
        with succ m' => (
            match n
                with zero => zero
                with succ n' => sub n' m'
        )

def is_zero : Nat -> Bool = fun n =>
    match n
        with zero => true
        with succ x => false

def less_than_eq : Nat -> Nat -> Bool = fun n m =>
    match n
        with zero => true
        with succ n' => (
            match m
                with zero => false
                with succ m' => less_than_eq n' m'
        )

def less_than : Nat -> Nat -> Bool = fun n m =>
    less_than_eq (succ n) m

def rem : Nat -> Nat -> Nat = fun n m =>
    match less_than n m
        with true => n
        with false => rem (sub n m) m

def eq : Nat -> Nat -> Bool = fun n m =>
    match n
        with zero => (
            match m
                with zero => true
                with succ x => false
        )
        with succ n' => (
            match m
                with zero => false
                with succ m' => eq n' m'
        )

def main : Top = println (show (add two three))