proposition: Lemma fsetD_eq0 (A B : {fset K}) : (A `\` B == fset0) = (A `<=` B).
proof: Proof. apply/fset_eqP/fsubsetP => sAB a. by move=> aA; have := sAB a; rewrite !inE aA andbT => /negPn. by rewrite !inE andbC; apply/negP => /andP [/sAB ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)