Follow-up from "WIP: Base for the behavior part of refactored PROSA." : Separate "facts" files

The following discussion from !12 (merged) should be addressed:

• @bbb started a discussion: (+2 comments)

  The trailing _cat in the lemma's name is (I believe) an ssreflect idiom and without prior exposure to this convention not intuitively readable. In the interest of readability, this should be either explained in the preceding comment or omitted.