proof.hs

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}

data Nat = Z | S Nat

data m <= n where
  Le_z :: (n <= n)
  Le_s :: (m <= n) -> (m <= S n)

type (m < n) = (S m <= n)

theorem :: (m < S n) -> (m <= n)
theorem prf =
  case prf of
    Le_z -> Le_z
    Le_s prf1 -> lemma_1 prf1

lemma_1 :: (S m <= n) -> (m <= n)
lemma_1 prf =
  case prf of
    Le_z -> Le_s Le_z
    Le_s prf1 -> Le_s $ lemma_1 prf1