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