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