Description
Thinking about #2558 / #2553 has led me to the conclusion that this lemma (introduced rather hastily by me in its current form during the refactoring of Data.Nat.Primality.Factorisation #1969, cf. also #2498) belongs not under Permutation.Setoid.Properties, but would fit 'better' in a scope where (Commutative)Monoid is already part of the ambient mathematical context, viz. as a(n additional) property of the Foldable structure on List.
Separately, and perhaps independent of the above consideration, the dependency structure of both the definition, and its use, is horrendous, relying as it does on the uneasy negotiation between the Structure and Bundle views of CommutativeMonoid, essentially only so that Relation.Binary.Reasoning.Setoid can be deployed... so there might be wider considerations of how we parametrise such modules... on the Bundle, or on the Structure (and the sense that it 'shouldn't matter', but alas, it does)?