proposition: Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
proof: Proof. induction n as [|n IH]. - by rewrite gmultiset_scalar_mul_0, gmultiset_size_empty. - rewrite gmultiset_scalar_mul_S_l, gmultiset_size_disj_union, IH. lia. Qed.
imports: stdpp(gmap) stdpp(options)