proposition: Lemma homg_trans aT (B : {set aT}) rT (C : {set rT}) gT (G : {group gT}) : homg C B -> homg B G -> homg C G.
proof: Proof. move=> homCB homBG; case/homgP: homBG homCB => fG <- /homgP[fK <-]. by rewrite -morphim_comp morphim_homg // -sub_morphim_pre. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)