proposition: Lemma misom_isog f : misom f -> isog.
proof: Proof. case/andP=> fM iso_f; apply/existsP; exists (finfun f). apply/andP; split; last by rewrite /misom /isom !(eq_imset _ (ffunE f)). by apply/forallP=> u; rewrite !ffunE; apply: forallP fM u. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)