Using the notion of permutations defined in this exercise and the counting function defined in this exercise. show that if a list is a permutation of another list, then any natural number occurs as many times in both lists.
Build a specialized reflection tactic ``\citecoq{NoPerm \(n\)}'' that solve goals of the form ~perm l l' by finding an element of the first list that does not occur the same number of times in both lists.