proposition: Lemma factmE x : x \in G -> ff (q x) = f x.
proof: Proof. rewrite /ff => Gx; have Hx := subsetP sGH x Gx. have /mem_repr: x \in q @*^-1 [set q x] by rewrite !inE Hx /=. case/morphpreP; move: (repr _) => y Hy /set1P. by case/ker_rcoset=> // z Kz ->; rewrite mkerl ?(subsetP sKqKf). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)