proposition: Lemma msubsetIidl A B : (A `<=` A `&` B) = (A `<=` B).
proof: Proof. apply/msubsetP/msubsetP=> sAB a; have := sAB a; rewrite !msetE. by rewrite leq_min leqnn. by move/minn_idPl->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap