Disable `succ_inj` at Algorithm World 5

[evrimoztamur]

The point of this one is to prove succ_inj, but we receive it earlier in the series and you can just... use it and then move on.

From what I understand there isn't a mechanic in lean4game which can re-block the dictionary items. I can assist with an implementation if helpful, thanks!

[joneugster]

Thanks for the comment! It is just succ_inj that's needs to be disabled, isn't it?

So adding DisabledTheorem MyNat.succ_inj as in the commit above should do.