proposition: Lemma E : setT = [set a; b].
proof: Proof. apply/setP => x; rewrite !inE; apply/esym; move: x. by apply: (@ind (fun x => (x == a) || (x == b))); rewrite eqxx ?orbT ?orTb. Qed.
imports: mathcomp(all_ssreflect fingroup perm)