proposition: Lemma isog_symr : G \isog H -> H \isog G.
proof: Proof. by case/isog_isom=> f /isom_sym/isom_isog->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)