For what it's worth, I proposed this as a 7kyu kata :)
I also agree with the above comment that theorem proving kata can have different sorts of difficulty, but I think this particular one is mathematically fairly straightforward.

I agree with the statement of ipergenitsa above. Perhaps, for Coq and other theorem proving tools, it would be a good idea to differentiate between different aspects of the katas complexity (with a tag ?):

• Program and prove: the main difficulty is to write and prove a program
• Mathematics: the main difficulty is to find the proof in theoretical maths (I mean that translating it into Coq is easy but the reasonning is hard)
• Logicians and tricks of Coq: the main difficulty is to know the very last features of the tool and the exact logic it relies on.

I think this particular problem would fall into the second category meaning that it is significantly harder for someone with a small background in mathematics. I personally struggled with problems of the third category (for example one using the very new feature of polymorphic universes in Coq).
Note that I may have missed the relevant tags and the respective meaning of 8kyu/7kyu etc (pointers are welcome ;) )

I agree that it should be 7kyu. But as I said, ranks can't be changed. It's 8kyu for non-beginners. ;-)

The task was probably ranked without concern for users who have no idea what theorem proving is, also regarding your first sentence, to put it bluntly, no one forces you to do so.

It's not the author's decision about the rank, and also, they can't be changed.

Yes.