proposition: Lemma morphim_fixP A : A \subset G -> reflect (f @* A = A) (f @* A \subset A).
proof: Proof. rewrite /morphim => sAG; have:= eqEcard (f @: A) A. rewrite (setIidPr sAG) card_in_imset ?leqnn ?andbT => [<-|]; first exact: eqP. by move/injmP: injf; apply: sub_in2; apply/subsetP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)