proposition: Lemma cards1P A : reflect (exists x, A = [set x]) (#|A| == 1).
proof: Proof. apply: (iffP idP) => [|[x ->]]; last by rewrite cards1. by have [[|x []]// _] := cards_eqP; exists x; apply/setP => y; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)