{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where

import Data.Word
import Test.Exhaustively

main :: IO ()
main = do
  r <- exhaustively (\(a::Word32) -> (a-1) < a)
  if r
    then pure ()
    else error "Did not prove!"