---------------------
--- Unary Numbers ---
---------------------
defn natural : prop
| zero = natural
| succ = natural -> natural
defn add : natural -> natural -> natural -> prop
>| add_z = add zero N N
>| add_s = add N M R -> add (succ N) M (succ R)
-- sub N M R is N - M = R
defn sub : natural -> natural -> natural -> prop
>| sub_by_add = sub N M R <- add M R N
fixity none 3 =<
defn =< : natural -> natural -> prop
>| leqZero = {B} zero =< B
>| leqSucc = {A B} (succ A) =< (succ B) <- A =< B
fixity none 3 <
defn < : natural -> natural -> prop
>| ltZero = zero < succ B
>| ltSucc = succ A < succ B <- A < B
defn odd : natural -> prop
>| odd/one = odd (succ zero)
>| odd/n = even A -> odd (succ A)
defn even : natural -> prop
>| even/zero = even zero
>| even/succ = odd B -> even (succ B)