proposition: Lemma isog_set1X (H2 : {group gT2}) : isog H2 (setX 1 H2).
proof: Proof. apply/isogP; exists [morphism of restrm (subsetT H2) pair1g]. by rewrite injm_restrm ?injm_pair1g. by rewrite morphim_restrm morphim_pair1g setIid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)