-- natural numbers defined by s-terms (Z=zero, S=successor):
data Nat = Z | S Nat
-- addition on natural numbers:
add :: Nat -> Nat -> Nat
add Z n = n
add (S m) n = S(add m n)
-- subtraction defined by reversing the addition:
sub x y | add y z =:= x = z where z free
-- less-or-equal predicated on natural numbers:
leq Z _ = True
leq (S _) Z = False
leq (S x) (S y) = leq x y
goal1 = sub (S(S(S(S Z)))) (S(S Z))
goal2 = findall (\x -> leq x (S(S Z)) =:= True)