proposition: Lemma isogP : reflect (exists2 f : {morphism G >-> rT}, 'injm f & f @* G = H) (G \isog H).
proof: Proof. apply: (iffP idP) => [/isog_isom[f /isomP[]] | [f injf fG]]; first by exists f. by apply: (isom_isog f) => //; apply/isomP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)