proposition: Lemma munion_rotate : forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
proof: Proof. intros; apply (op_rotate multiset munion meq). - apply munion_comm. - apply munion_ass. - exact meq_trans. - exact meq_sym. - trivial. Qed.
imports: PeanoNat Permut Setoid