proposition: Lemma set1_set2 A (E : {set A}) a : a \in E -> E != set1 a -> exists i, (i \in E) && (i != a).
proof: Proof. move/setD1K => aC Ca. have /set0Pn[b] : E :\ a != set0. apply: contra Ca; rewrite setD_eq0 subset1 => /orP[//|]. by rewrite -aC => /eqP/setP/(_ a); rewrite !inE eqxx. rewrite !inE => /andP[ba bC]; exists b; by rewrite bC. Qed.
imports: mathcomp(all_ssreflect fingroup perm)