proposition: Lemma TI_Ohm1 G H : H :&: 'Ohm_1(G) = 1 -> H :&: G = 1.
proof: Proof. move=> tiHG1; case: (trivgVpdiv (H :&: G)) => // [[p pr_p]]. case/Cauchy=> // x /setIP[Hx Gx] ox. suffices x1: x \in [1] by rewrite -ox (set1P x1) order1 in pr_p. by rewrite -{}tiHG1 inE Hx Ohm1Eprime mem_gen // inE Gx ox. 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)