proposition: Lemma cardsltn1P A (E : {set A}) : (1 < #| E |) = [exists a, exists b, [&& (a \in E), (b \in E) & (a != b)]].
proof: Proof. case/boolP : (E == set0) => [/eqP -> | /set0Pn [] /= a Ha]. rewrite cards0; apply/esym/negbTE. rewrite negb_exists; apply/forallP => a. rewrite negb_exists; apply/forallP => b; by rewrite !inE. case/boolP : (E :\ a == set0) => [/eqP Ea0 | ]. have -> : E = [set a] by apply/eqP; rewrite -(setD1K Ha) Ea0 setU0. rewrite cards1; apply/esym/negbTE. rewrite negb_exists; apply/forallP => b. rewrite negb_exists; apply/forallP => c. rewrite 2!in_set1 2!negb_and negbK. case/boolP : (b == c) => [_|bc]; first by rewrite !orbT. rewrite orbF. case/boolP : (b == a) => //= /eqP <-; by rewrite eq_sym. case/set0Pn => b Hb. have -> : 1 < #| E | by rewrite (cardsD1 a E) Ha /= (cardsD1 b (E :\ a)) Hb. apply/esym; apply/existsP; exists a; apply/existsP; exists b. by rewrite !inE eq_sym andbC in Hb; rewrite Hb Ha. Qed.
imports: mathcomp(all_ssreflect fingroup perm)