proposition: Lemma morphimV A : f @* A^-1 = (f @* A)^-1.
proof: Proof. wlog suffices: A / f @* A^-1 \subset (f @* A)^-1. by move=> IH; apply/eqP; rewrite eqEsubset IH -invSg invgK -{1}(invgK A) IH. apply/subsetP=> _ /morphimP[x Dx Ax' ->]; rewrite !inE in Ax' *. by rewrite -morphV // imset_f // inE groupV Dx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)