-- To detect the non-failure of the following operation,
-- reasoning over integers is required:
abs :: Int -> Int
abs x | x>=0 = x
      | x<0  = 0 - x

-- It must be proved that the guards are complete since the definition
-- above is translated into the following definition:
absif :: Int -> Int
absif x = if x>=0 then x
                  else if x<0 then (0 - x)
                              else failed