proposition: Lemma meq_right : forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
proof: Proof. unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z. intros; elim H; auto. Qed.
imports: PeanoNat Permut Setoid