module HomeworkTen
%default total

data Less : Nat -> Nat -> Type where
  Suc : Less n (S n)
  Trans : Less k n -> Less n m -> Less k m

data Sorted : List Nat -> Type where
  SortedEmpty : Sorted []
  SortedSingle : Sorted [x]
  SortedCons : Less x y -> Sorted (y::tail) -> Sorted (x::y::tail)

threeLessThanFive : Less 3 5
threeLessThanFive = Trans Suc Suc

threeFiveSorted : Sorted [3,5]
threeFiveSorted = SortedCons threeLessThanFive SortedSingle

tailSorted : Sorted (x::xs) -> Sorted xs
tailSorted SortedEmpty impossible
tailSorted SortedSingle = SortedEmpty
tailSorted (SortedCons _ st) = st

firstSecondLess : Sorted (x::y::xs) -> Less x y
firstSecondLess SortedEmpty impossible
firstSecondLess SortedSingle impossible
firstSecondLess (SortedCons l _) = l

removeSecondSorted : Sorted (x::y::xs) -> Sorted (x::xs)
removeSecondSorted SortedEmpty impossible
removeSecondSorted SortedSingle impossible
removeSecondSorted (SortedCons _ SortedEmpty) impossible
removeSecondSorted (SortedCons _ SortedSingle) = SortedSingle
removeSecondSorted (SortedCons lxy (SortedCons lyr t)) = SortedCons (Trans lxy lyr) t