proposition: Lemma morphim_factm (A : {set aT}) : ff @* (q @* A) = f @* A.
proof: Proof. rewrite -morphim_comp /= {1}/morphim /= morphimGK //; last first. by rewrite (subset_trans sKqKf) ?subsetIl. apply/setP=> y; apply/morphimP/morphimP; by case=> x Gx Ax ->{y}; exists x; rewrite //= factmE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)