proposition: Lemma mset1UE a A b : (a |` A) b = maxn (b == a) (A b).
proof: Proof. by rewrite msetE2 msetnE; case: (b == a). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap