/*
 * supplied as a separate function because - is a UNARY symbol in Cora's integer
 * theory, so passing as an argument to [-] to comp would not work as desired
 */
minus :: Int -> Int -> Int
minus(x, y) → x - y

readint :: (Int -> Int) -> Int
readint(k) -> k(n)

comp :: ((Int -> Int) -> Int) -> (Int -> (Int -> Int)) -> Int -> Int
comp(f, g, x) → f(g(x))

sub :: Int
sub -> readint(comp(readint, minus))