proposition: Lemma multiplicity_singleton' x y : multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
proof: Proof. destruct (decide _) as [->|]. - by rewrite multiplicity_singleton. - by rewrite multiplicity_singleton_ne. Qed.
imports: stdpp(gmap) stdpp(options)