proposition: Lemma isog_abelian : G \isog H -> abelian G = abelian H.
proof: Proof. by case/isogP=> f injf <-; rewrite injm_abelian. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)