proposition: Lemma misomP f : reflect {fM : morphic f & isom (morphm fM)} (misom f).
proof: Proof. by apply: (iffP andP) => [] [fM fiso] //; exists fM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)