proposition: Lemma fsubset0 A : (A `<=` fset0) = (A == fset0).
proof: Proof. by rewrite eqEfsubset fsub0set andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)