data N  = Z | S (n :: N)

(+) (n,m:: N)
    :: N
    = case m of {
        (Z) -> n;
        (S m') -> S (n + m');}

-- False in Agda:
data False =

-- True in Agda:
data True = true


-- Equality on N
(==) (n,m::N)
     :: Set
      = case n of
            { (Z)       -> case m of
                                { (Z)     -> True;
                                  (S m')  -> False;};
              (S n')    -> case m of
                                { (Z)     -> False;
                                  (S m')  -> n' == m';};}

-- Less Than
(<) (n,m :: N)
    :: Set
     = case n of {
         (Z) -> case m of {
                  (Z) -> False;
                  (S m') -> True;};
         (S n') -> case m of {
                     (Z) -> False;
                     (S m') -> n' < m';};} 



one :: N
   = S Z

mono (n,k,m :: N)
     (p :: n < k)
     :: (n + m) < (k + m)
     = case n of {
         (Z) -> case k of {
                  (Z) -> case p of { };
                  (S k') -> case m of {
                              (Z) -> true;
                              (S m') -> mono n k m' p;};};
         (S n') -> case k of {
                     (Z) -> case p of { };
                     (S k') -> case m of {
                                 (Z) -> p;
                                 (S m') -> mono n k m' p;};};}