content: -- % cabal install hspec
  -- % runghc <this_file>
  
  import Nat
  import Small
  
  main :: IO ()
  main = hspec $ do
      describe "my_plus_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= 0 && n >= 0
          ==> my_from_n (my_to_n m `my_plus_n` my_to_n n) == m + n
      describe "my_minus_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= n && n >= 0
          ==> my_from_n (my_to_n m `my_minus_n` my_to_n n) == m - n
      describe "my_mul_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= 1 && n >= 1
          ==> my_from_n (my_to_n m `my_mul_n` my_to_n n) == m * n
      describe "my_lt_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= 0 && n >= 0
          ==> my_to_n m `my_lt_n` my_to_n n == (m < n)
      describe "my_divide_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= 0 && n >= 1
          ==> my_from_n (my_to_n m `my_divide_n` my_to_n n) == m `div` n
      describe "my_remainder_n" $
        prop "behaves as model" $ \(Small m) (Small n) -> m >= 0 && n >= 1
          ==> my_from_n (my_to_n m `my_remainder_n` my_to_n n) == m `mod` n
  
  my_plus_n :: Nat -> Nat -> Nat
  my_plus_n m n
    | my_isZero_n n = m
    | otherwise     = my_plus1_n (m `my_plus_n` my_minus1_n n)
  
  my_isOne_n :: Nat -> Bool
  my_isOne_n n
    | my_isZero_n n               = False
    | my_isZero_n (my_minus1_n n) = True
    | otherwise                   = False
  
  my_mul_n :: Nat -> Nat -> Nat
  my_mul_n m n
    | my_isOne_n n = m
    | otherwise    = my_mul_n m (my_minus1_n n) `my_plus_n` m
  
  my_minus_n :: Nat -> Nat -> Nat
  my_minus_n m n
    | my_isZero_n n = m
    | otherwise     = my_minus1_n (m `my_minus_n` my_minus1_n n)
  
  my_lt_n :: Nat -> Nat -> Bool
  my_lt_n m n
    | my_isZero_n n = False
    | my_isZero_n m = True
    | otherwise = my_lt_n (my_minus1_n m) (my_minus1_n n)
  
  my_divide_n :: Nat -> Nat -> Nat
  my_divide_n m n
    | m `my_lt_n` n = my_zero_n
    | otherwise     = my_plus1_n ((m `my_minus_n` n) `my_divide_n` n)
  
  my_remainder_n :: Nat -> Nat -> Nat
  my_remainder_n m n
    | m `my_lt_n` n = m
    | otherwise     = my_remainder_n (m `my_minus_n` n) n
  