Pigeonhole Principle in Idris

PigeonHole.idr

module PigeonHole

import Data.Nat
import Data.Vect

%default total

data Elem : a -> Vect k a -> Type where
  Here : Elem x (x :: xs)
  There : Elem x xs -> Elem x (y :: xs)

sum' : Vect k Nat -> Nat
sum' [] = 0
sum' (x :: xs) = S (sum' xs)

pigeonHole : (xs : Vect k Nat) -> (prf : LTE (S k) (PigeonHole.sum' xs)) -> (n : Nat ** (Elem n xs, LTE 2 n))
pigeonHole [] prf = absurd prf
pigeonHole (x :: xs) prf = 
  case isLTE 2 x of
    No contra => 
      let (m ** (prf', prf2')) = pigeonHole xs (fromLteSucc prf)
      in (m ** (There prf', prf2'))
    Yes p => (x ** (Here, p))