proposition: Lemma fsubsetP {A B} : reflect {subset A <= B} (A `<=` B).
proof: Proof. apply: (iffP fset_eqP) => AsubB a; first by rewrite -AsubB inE => /andP[]. by rewrite inE; have [/AsubB|] := boolP (a \in A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)