proposition: Lemma morphim_qisom_inj : injective (fun Gx => qisom @* Gx).
proof: Proof. by move=> Gx Gy; apply: injm_morphim_inj; rewrite (injm_qisom, subsetT). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)