proposition: Lemma isog_isom : isog -> {f : {morphism A >-> rT} | isom f}.
proof: Proof. by case/existsP/sigW=> f /misomP[fM isom_f]; exists (morphm_morphism fM). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)