proposition: Lemma gmultiset_elements_disj_union X Y : elements (X ⊎ Y) ≡ₚ elements X ++ elements Y.
proof: Proof. destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements. set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl. revert Y; induction X as [|x n X HX IH] using map_ind; intros Y. { by rewrite (left_id_L _ _ Y), map_to_list_empty. } destruct (Y !! x) as [n'|] eqn:HY. - rewrite <-(insert_delete Y x n') by done. erewrite <-insert_union_with by done. rewrite !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX). rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH. rewrite (assoc_L _). f_equiv. rewrite (comm _); simpl. by rewrite Pos2Nat.inj_add, replicate_add. - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?HX, ?HY). by rewrite <-(assoc_L (++)), <-IH. Qed.
imports: stdpp(gmap) stdpp(options)