lemma_fold_right_permutation proves that, when doing a fold_right with a commutative operator, any permutation of the sequence produces the same result.
to_multiset_remove strengthens to_multiset_ensures() to reason about removing elements from a seq.
lemma_multiset_has_no_duplicates_conv is the converse of lemma_multiset_has_no_duplicates and helps prove that, if a sequence was no_duplicates(), then any permutation (with an equal to_multiset()) also has no_duplicates().
The main lemmas of interest here are:
lemma_fold_right_permutationproves that, when doing afold_rightwith a commutative operator, any permutation of the sequence produces the same result.to_multiset_removestrengthensto_multiset_ensures()to reason about removing elements from a seq.lemma_multiset_has_no_duplicates_convis the converse oflemma_multiset_has_no_duplicatesand helps prove that, if a sequence wasno_duplicates(), then any permutation (with an equalto_multiset()) also hasno_duplicates().