proposition: Lemma der_cprod n A B G : A \* B = G -> A^`(n) \* B^`(n) = G^`(n).
proof: Proof. by move=> defG; elim: n => {defG}// n; apply: (lcn_cprod 2). 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)