proposition: Lemma gmultiset_elements_scalar_mul n X : elements (n *: X) ≡ₚ mjoin (replicate n (elements X)).
proof: Proof. induction n as [|n IH]; simpl. - by rewrite gmultiset_scalar_mul_0, gmultiset_elements_empty. - by rewrite gmultiset_scalar_mul_S_l, gmultiset_elements_disj_union, IH. Qed.
imports: stdpp(gmap) stdpp(options)