proposition: Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
proof: Proof. unfold meq; unfold multiplicity; unfold munion. destruct x; destruct y; intros; apply Nat.add_comm. Qed.
imports: PeanoNat Permut Setoid