proposition: Lemma cardfs0_eq A : #|` A| = 0 -> A = fset0.
proof: Proof. by move=> /eqP; rewrite cardfs_eq0 => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)