proposition: Lemma morphpre_factm (C : {set rT}) : ff @*^-1 C = q @* (f @*^-1 C).
proof: Proof. apply/setP=> y /[!inE]/=; apply/andP/morphimP=> [[]|[x Hx]]; last first. by case/morphpreP=> Gx Cfx ->; rewrite factmE ?imset_f ?inE ?Hx. case/morphimP=> x Hx Gx ->; rewrite factmE //. by exists x; rewrite // !inE Gx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)