#17688: fix declaration for richcmp example in the docs.

Thanks to Daniel Mullner