Variation on Miles's increasing seq, this is a decreasing seq

gistfile1.scala

object Generics {
  import shapeless.HList
  import shapeless.Nat
  import shapeless.Nat._
  import shapeless._

  trait <[A <: Nat, B <: Nat]
  implicit def lt1[B <: Nat] = new <[_0, Succ[B]] {}
  implicit def lt2[A <: Nat, B <: Nat](implicit lt: A < B) = new <[Succ[A], Succ[B]] {}

  trait Increasing[L <: HList]
  implicit def hnilIncreasing = new Increasing[HNil] {}
  implicit def hlistIncreasing1[H] = new Increasing[H :: HNil] {}
  implicit def hlistIncreasing2[H1 <: Nat, H2 <: Nat, T <: HList](implicit lt: H1 < H2, it: Increasing[H2 :: T]) = new Increasing[H1 :: H2 :: T] {}

  def acceptIncreasing[L <: HList](l: L)(implicit i: Increasing[L]) = l

  // Verify type-level relations
  implicitly[Increasing[_1 :: _2 :: _3 :: HNil]] // OK
  // implicitly[Increasing[_1 :: _3 :: _2 :: HNil]] // Does not compile

  // Apply at the value-level
  acceptIncreasing(_1 :: _2 :: _3 :: HNil) // OK
  // acceptIncreasing(_1 :: _3 :: _2 :: HNil)       // Does not compile

  trait Decreasing[L <: HList]
  implicit def hnilDecreasing = new Decreasing[HNil] {}
  implicit def hlistDecreasing1[H] = new Decreasing[H :: HNil] {}
  implicit def hlistDecreasing2[H1 <: Nat, H2 <: Nat, T <: HList](implicit gt: Pred[H1, H2], it: Decreasing[H2 :: T]) = new Decreasing[H1 :: H2 :: T] {}

  
  implicitly[Decreasing[_3 :: _2 :: _1 :: HNil]]
  implicitly[Decreasing[HNil]] // empty list
  //implicitly[Decreasing[_1 :: _3 :: _2 :: HNil]] // does not compile
}