I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.

Fixed

Fixed

Same for Coq. As far as I can tell there is no way to inspect the Preloded file, and the interface of codewards is completely inadequate. I managed to find the required definitions by Printing their names and "attempting" to solve the problem, which then shows the result of running the file. But this is really suboptimal.

Edit: Ok, my bad, the definitions are provided in the comments of the problem. This still strikes me as a weird way to do it.

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

Fixed

Fixed

This Kata is not compatible with Lean v3.18.4 as of 16/08/2020 and needs to be upgraded.

This Kata is not compatible with Lean v3.18.4 as of 16/08/2020 and needs to be upgraded.

The extra cases n used here to make the -1s easier to get rid of is sweet! It's a very convenient way of replacing every n in a goal with n.succ.

No worries - just leave it for now then.

If this comment is addressed to me, I am not sure I am confident enough with Coq syntax any more to know whether what you have done is OK (I haven't used Coq for about 2 years and I quickly forget things which I don't use a lot).