proposition: Lemma morphim_fstX (H1: {set gT1}) (H2 : {group gT2}) : [morphism of fun x => x.1] @* setX H1 H2 = H1.
proof: Proof. apply/eqP; rewrite eqEsubset morphimE setTI /=. apply/andP; split; apply/subsetP=> x. by case/imsetP=> x0 /[1!inE] /andP[Hx1 _] ->. move=> Hx1; apply/imsetP; exists (x, 1); last by trivial. by rewrite in_setX Hx1 /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)