proposition: Lemma lcn_cprod n A B G : A \* B = G -> 'L_n(A) \* 'L_n(B) = 'L_n(G).
proof: Proof. case: n => // n /cprodP[[H K -> ->{A B}] defG cHK]. have sL := subset_trans (lcn_sub _ _); rewrite cprodE ?(centSS _ _ cHK) ?sL //. symmetry; elim: n => // n; rewrite lcnSn => ->; rewrite commMG /=; last first. by apply: subset_trans (commg_normr _ _); rewrite sL // -defG mulG_subr. rewrite -!(commGC G) -defG -{1}(centC cHK). rewrite !commMG ?normsR ?lcn_norm ?cents_norm // 1?centsC //. by rewrite -!(commGC 'L__(_)) -!lcnSn !(commG1P _) ?mul1g ?sL // centsC. 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)