Comment by antpls

Is that the same proof than the ~120 lines of code of the link?

If yes, proof assistants have to be improved on conciseness, imho