proposition: Lemma fsetUidPr A B : reflect (A `|` B = B) (A `<=` B).
proof: Proof. apply: (iffP fsubsetP) => sAB; last by move=> a aA; rewrite -sAB inE aA. by apply/fsetP => b; rewrite inE; have [/sAB|//] := boolP (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)