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