proposition: Lemma cprod_nil A B G : A \* B = G -> nilpotent G = nilpotent A && nilpotent B.
proof: Proof. move=> defG; case/cprodP: defG (defG) => [[H K -> ->{A B}] defG _] defGc. apply/idP/andP=> [nilG | [/lcnP[m LmH1] /lcnP[n LnK1]]]. by rewrite !(nilpotentS _ nilG) // -defG (mulG_subr, mulG_subl). apply/lcnP; exists (m + n.+1); apply/trivgP. case/cprodP: (lcn_cprod (m.+1 + n.+1) defGc) => _ <- _. by rewrite mulG_subG /= -{1}LmH1 -LnK1 !lcn_sub_leq ?leq_addl ?leq_addr. 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)