proposition: Lemma gmultiset_set_fold_scalar_mul (f : A → A → A) (b : A) n X : Comm (=) f → Assoc (=) f → set_fold f b (n *: X) = Nat.iter n (flip (set_fold f) X) b.
proof: Proof. intros Hcomm Hassoc. induction n as [|n IH]; simpl. - by rewrite gmultiset_scalar_mul_0, gmultiset_set_fold_empty. - rewrite gmultiset_scalar_mul_S_r. by rewrite (gmultiset_set_fold_disj_union _ _ _ _ _ _), IH. Qed.
imports: stdpp(gmap) stdpp(options)