Generic type matching

Can this code be tweaked so that it compiles?

In it, I first define type-level natural numbers:

sealed trait NatT
case class Zero() extends NatT
case class Succ[N<: NatT](n: N) extends NatT

Then, I define a comparison predicate:

trait IsLessThan[M <: NatT, N <: NatT]
object IsLessThan:
  given base[M <: NatT]: IsLessThan[M, Succ[M]]()
  given weakening[N <: NatT, M <: NatT] (using IsLessThan[N, M]): IsLessThan[N, Succ[M]]()
  given reduction[N <: NatT, M <: NatT] (using IsLessThan[Succ[N], Succ[M]]): IsLessThan[N, M]()

Finaly, I define UniformTuple. I want it to have a method to get the ith element of the tuple, and I want the method to be fully type-safe (no possible runtime exceptions due to out-of-bound indices), so the method demands a proof that the index is within bounds:

sealed trait UniformTuple[Length <: NatT, T]:
  def apply[M <: NatT](m: M)(using IsLessThan[M, Length]): T

case class Empty[T: Fractional]() extends UniformTuple[Zero, T]:
  def apply[M <: NatT](m: M)(using IsLessThan[M, Zero]): T = throw new AssertionError("Uncallable")

case class Cons[N <: NatT, T: Fractional](head: T, tail: UniformTuple[N, T]) extends UniformTuple[Succ[N], T]:
  def apply[M <: NatT](m: M)(using proof: IsLessThan[M, Succ[N]]): T = m match
    case Zero() => head
    case Succ(predM): Succ[predM] => tail(predM)(using IsLessThan.reduction(using proof))

However, I cannot get the recursion to go through, as the compiler apparently doesn’t know that Succ[predM] is the same as M