proposition: Lemma Ohm_cont rT G (f : {morphism G >-> rT}) : f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).
proof: Proof. rewrite morphim_gen ?genS //; last by rewrite -gen_subG Ohm_sub. apply/subsetP=> fx /morphimP[x Gx]; rewrite inE Gx /=. case/OhmPredP=> p p_pr xpn_1 -> {fx}. rewrite inE morphimEdom imset_f //=; apply/OhmPredP; exists p => //. by rewrite -morphX // xpn_1 morph1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)