caledon-3.2.0.0: prelude/naturals.ncc

---------------------
--- 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)