proposition: Lemma isom_sym (f : {morphism G >-> hT}) (isoGH : isom G H f) : isom H G (isom_inv isoGH).
proof: Proof. rewrite sub_isom 1?injm_restrm ?injm_invm // im_restrm. by rewrite -(isom_im isoGH) im_invm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)