proposition: Lemma injm_qisom : 'injm qisom.
proof: Proof. by rewrite -quotient1 -morphpre_qisom morphpreS ?sub1G. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)