proposition: Lemma set2_set1 A (E : {set A}) a : (exists i, (i \in E) && (i != a)) -> E != set1 a.
proof: Proof. case=> b /andP[bC]; apply: contra => /eqP Ca; move: bC; by rewrite Ca !inE. Qed.
imports: mathcomp(all_ssreflect fingroup perm)