proposition: Lemma cyclic_pgroup_dprod_trivg p A B C : p.-group C -> cyclic C -> A \x B = C -> A = 1 /\ B = C \/ B = 1 /\ A = C.
proof: Proof. move=> pC cycC; case/cyclicP: cycC pC => x ->{C} pC defC. case/dprodP: defC => [] [G H -> ->{A B}] defC _ tiGH; rewrite -defC. have [/trivgP | ntC] := eqVneq <[x]> 1. by rewrite -defC mulG_subG => /andP[/trivgP-> _]; rewrite mul1g; left. have [pr_p _ _] := pgroup_pdiv pC ntC; pose K := 'Ohm_1(<[x]>). have prK : prime #|K| by rewrite (Ohm1_cyclic_pgroup_prime _ pC) ?cycle_cyclic. case: (prime_subgroupVti G prK) => [sKG |]; last first. move/TI_Ohm1; rewrite -defC (setIidPl (mulG_subl _ _)) => ->. by left; rewrite mul1g. case: (prime_subgroupVti H prK) => [sKH |]; last first. move/TI_Ohm1; rewrite -defC (setIidPl (mulG_subr _ _)) => ->. by right; rewrite mulg1. have K1: K :=: 1 by apply/trivgP; rewrite -tiGH subsetI sKG. by rewrite K1 cards1 in prK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)