proposition: Lemma lcn_cont n : GFunctor.continuous (@lower_central_at n).
proof: Proof. case: n => //; elim=> // n IHn g0T h0T H phi. by rewrite !lcnSn morphimR ?lcn_sub // commSg ?IHn. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)