i will see what i can do :3

see, i had originally tried to model jealousy as a separate relation which occurs if A's butt is less enviable than B's and A is insecure about their own butt, because relying entirely on the existing partial order relation of the numerical enviability value seemed kinda cheap. the problem which i didn't realize until getting a good way into it is that in that model, jealousy is not transitive, so i simplified everything until i had a minimal example which actually fulfills the original premise. now i have two formally proven lemmas which appear to be completely useless...

side note, if i type "A" and spam autocomplete my phone now writes "A's butt is less enviable than B's butt", which i think is beautiful