proposition: Lemma cardfs1P A : reflect (exists x, A = [fset x]) (#|` A| == 1).
proof: Proof. apply: (iffP idP) => [|[x ->]]; last by rewrite cardfs1. rewrite eq_sym eqn_leq cardfs_gt0=> /andP[/fset0Pn[x Ax] leA1]. by exists x; apply/eqP; rewrite eq_sym eqEfcard fsub1set cardfs1 leA1 Ax. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)