proposition: Lemma srelE S1 S2 : srel S1 =2 srel S2 -> S1 = S2.
proof: Proof. by move=> eqS; apply/setP => [[x y]]; apply: eqS x y. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr