proposition: Lemma morphim_der rT D (f : {morphism D >-> rT}) n G : G \subset D -> f @* G^`(n) = (f @* G)^`(n).
proof: Proof. move=> sGD; elim: n => // n IHn. by rewrite !dergSn -IHn morphimR ?(subset_trans (der_sub n G)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)