proposition: Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) (#|A| == 2).
proof: Proof. apply: (iffP idP) => [|[x] [y] [xy ->]]; last by rewrite cards2 xy. have [[|x [|y []]]//=] := cards_eqP; rewrite !inE andbT => neq_xy. by exists x, y; split=> //; apply/setP => z; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)