The Coq version of this kata requires a constructive proof.
Yeah, I think it would be somewhat interesting, but might also have negative side effects of spreading the misconception that constructive code is central to interactive theorem proving.
I see, thanks for explaining, thats a little unfortunate, would be cool to be able to actually test for constructive kata.
This comment is hidden because it contains spoiler information about the solution
A good patch is to have
in the header of any Lean kata which is meant to be about "everyday mathematics".
I don't think "learn Lean entirely through exercises on Codewars" is a particularly good life strategy, anymore than it would be for learning other languages. Come ask questions here
or use this website to find reference material
I've edited the kata after authoring the translation so you might get a description merge conflict when trying to approve the original translation. In that case, you may wish to approve this fork instead.
Coq Translation Kumited - please accept :-D
I think this would be better with z:\R instead of z:\Z.