Natural numbers in scala types

NatN in scala type.scala

sealed trait Nat {
  type plus[That <: Nat] <: Nat
}
sealed trait Nat0 extends Nat {
  type plus[That <: Nat] = That
}
sealed trait NatN[Prev <: Nat] extends Nat {
  type plus[That <: Nat] = NatN[Prev#plus[That]]
}
object Nat {
  type +[A <: Nat, B <: Nat] = A#plus[B]
}

object NatSpecs {
  import Nat._
  type Nat1 = NatN[Nat0]
  type Nat2 = NatN[Nat1]
  type Nat3 = NatN[Nat2]

  implicitly[Nat0 =:= Nat0]

  implicitly[Nat0 + Nat1 =:= Nat1]
}