proposition: Lemma msubUset A B C : (B `|` C `<=` A) = (B `<=` A) && (C `<=` A).
proof: Proof. apply/idP/idP => [subA|/andP [AB CA]]; last by rewrite -[A]msetUid msetUSS. by rewrite !(msubset_trans _ subA). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap