proposition: Lemma morphim_invmE C : invm @* C = f @*^-1 C.
proof: Proof. rewrite -morphpreIdom -(morphim_invm (subsetIl _ _)). by rewrite morphimIdom -morphpreIim morphpreK (subsetIl, morphimIdom). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)