proposition: Lemma fset_0Vmem A : (A = fset0) + {x : K | x \in A}.
proof: Proof. have [|[x mem_x]] := set_0Vmem (fsub A A); last first. by right; exists (val x); rewrite inE // in mem_x. by move=> /eqP; rewrite fsub_eq0 // => /eqP; left. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)