I don’t understand why the following code won’t compile.

```
sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT
type _1 = Succ[Zero]
type _2 = Succ[_1]
type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
case Zero => X
case Succ[y] => NatSum[Succ[X], y]
sealed trait NatDivides[X <: Succ[NatT], Y <: NatT]
object NatDivides:
given baseCase[X <: Succ[NatT]]: NatDivides[X, Zero]()
given inductiveCase[X <: Succ[NatT], Y <: NatT](using proof: NatDivides[X, Y]): NatDivides[X, NatSum[Y, X]]()
@main def main(): Unit =
summon[NatDivides[_1, _2]]
summon[NatDivides[_2, _2]]
```

I find it particularly odd since it does compile if I comment out the last line. I do not know how the compiler searches for a proof/instance of a type, but it seems to me that proving the last line should be easier than the line before it.