proposition: Lemma derJ G n x : (G :^ x)^`(n) = G^`(n) :^ x.
proof: Proof. by elim: n => //= n IHn; rewrite !dergSn IHn -conjsRg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)