proposition: Lemma fset0Pn A : reflect (exists x, x \in A) (A != fset0).
proof: Proof. rewrite -cardfs_eq0 cardfE; apply: (equivP existsP). by split=> [] [a aP]; [exists (val a); apply: valP|exists [` aP]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)