proposition: Lemma lcn_dprod n A B G : A \x B = G -> 'L_n(A) \x 'L_n(B) = 'L_n(G).
proof: Proof. move=> defG; have [[K H defA defB] _ _ tiAB] := dprodP defG. rewrite !dprodEcp // in defG *; first exact: lcn_cprod. by rewrite defA defB; apply/trivgP; rewrite -tiAB defA defB setISS ?lcn_sub. 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)