proposition: Lemma fsetU_eq0 A B : (A `|` B == fset0) = (A == fset0) && (B == fset0).
proof: Proof. by rewrite -!fsubset0 fsubUset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)