proposition: Lemma isog_transl : G \isog H -> (G \isog K) = (H \isog K).
proof: Proof. by move=> iso; apply/idP/idP; apply: isog_trans; rewrite // -isog_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)