Less than

lt.idr

-- We could define the relation like this:

data LessThan : Nat -> Nat -> Type where
     LT_Z : LessThan Z (S m)
     LT_S : LessThan n m -> LessThan (S n) (S m)

-- Then calculate a proof, if one exists:
  
isLessThan : (m : Nat) -> (n : Nat) -> Maybe (LessThan m n)
isLessThan Z Z = Nothing
isLessThan Z (S k) = Just LT_Z
isLessThan (S k) Z = Nothing
isLessThan (S k) (S j) = case isLessThan k j of
                              Nothing => Nothing
                              Just p => Just (LT_S p)
                              
-- Some examples:

{-

*lt> isLessThan 3 5
Just (LT_S (LT_S (LT_S LT_Z))) : Maybe (LessThan 3 5)

*lt> isLessThan 3 2
Nothing : Maybe (LessThan 3 2)

-}

{- P.S. A shorter way of writing the last case of isLessThan uses ! notation:

isLessThan (S k) (S j) = Just (LT_S !(isLessThan k j))

-}