This Kata is not compatible with Lean 3.20.c as of 08/10/2020
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.
This comment is hidden because it contains spoiler information about the solution
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).
Please do check out my Coq translation in your spare time - just click on the link and hit the "Approve" button at the top right hand corner if everything looks okay :-)
Coq Translation Kumited - please accept :-D
Either there is some issue with imports (the most likely -- even should be defined in preloaded) or there's a difference between Lean 3.5.1 (CoCalc) and Lean 3.7.2 (here) but that is vanishingly unlikely with kata at this level (cutting edge mathlib stuff changes but not basic stuff like this).
Edit: Oh, but I see you solved it :-)