proposition: Lemma invset_Delta s : invset s \subset Delta.
proof: Proof. rewrite /invset/Delta; apply/subsetP => [[/= i j]]. by rewrite !inE /= => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr