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