proposition: Lemma multiplicity_scalar_mul n X x : multiplicity x (n *: X) = n * multiplicity x X.
proof: Proof. destruct X as [X]; unfold multiplicity; simpl. destruct n as [|n]; [done|]. rewrite lookup_fmap. destruct (X !! _); simpl; lia. Qed.
imports: stdpp(gmap) stdpp(options)