proposition: Lemma invset_permV s : invset s^-1 = [set (s (p.2), s (p.1)) | p in invset s].
proof: Proof. apply/setP => [[i j]]; rewrite !inE /=. apply/andP/imsetP => /= [[Hij Hsij] | [] [u v]]. - by exists (s^-1 j, s^-1 i); rewrite ?inE ?Hsij ?permKV ?Hij. - by rewrite inE /= => /andP[Huv Hsuv] [-> ->]; rewrite !permK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr