proposition: Lemma msubset_subset {A B} : A `<=` B -> {subset A <= B}.
proof: Proof. by move=> /msubsetP AB x; rewrite !in_mset => ?; exact: (leq_trans _ (AB _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap