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.

which solution?

A good patch is to have

noncomputable theory
open_locale classical

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
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members

or use this website to find reference material
https://leanprover-community.github.io/

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.