proposition: Lemma cards2P (A : finType) (E : {set A}) : (#| E | == 2) = [exists a, exists b, (E == [set a; b]) && (a != b)].
proof: Proof. apply/idP/idP => [s2|]; last first. by move/existsP => -[a /existsP[b /andP[/eqP -> ab]]]; rewrite cards2 ab. move: (s2) => /eqP/esym/eq_leq. rewrite cardsltn1P => /existsP[a /existsP[b /and3P[aE bE ab]]]. apply/existsP; exists a; apply/existsP; exists b; rewrite ab andbT; apply/eqP. rewrite -(setD1K aE) -(setD1K bE); apply/setP => i; rewrite !inE. have [/eqP->{i} //|/= ia] := boolP (i == a). have [/eqP->{i} //|/= ib] := boolP (i == b). apply/negbTE/negP => iE. move/eqP : s2; rewrite (cardsD1 a) aE add1n => -[]. rewrite (cardD1 b) !inE eq_sym ab bE add1n => -[]. by rewrite (cardD1 i) !inE ib ia iE add1n. Qed.
imports: mathcomp(all_ssreflect fingroup perm)