proposition: Lemma morphpre_qisom A : qisom @*^-1 (A / H) = A / G.
proof: Proof. rewrite morphpre_restrm setTI morphpre_factm eqGH. by rewrite morphpreK // im_coset subsetT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)