proposition: Lemma msetUidPr A B : reflect (A `|` B = B) (A `<=` B).
proof: Proof. apply: (iffP msubsetP) => [AB|<- a]; last by rewrite !msetE leq_max leqnn. by apply/msetP=> a; rewrite !msetE (maxn_idPr _). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap