proposition: Lemma coprime_index_mulG G H K : H \subset G -> K \subset G -> coprime #|G : H| #|G : K| -> H * K = G.
proof: Proof. move=> sHG sKG co_iG_HK; apply/eqP; rewrite eqEcard mul_subG //=. rewrite -(@leq_pmul2r #|H :&: K|) ?cardG_gt0 // -mul_cardG. rewrite -(Lagrange sHG) -(LagrangeI K H) mulnAC setIC -mulnA. rewrite !leq_pmul2l ?cardG_gt0 // dvdn_leq // -(Gauss_dvdr _ co_iG_HK). by rewrite -(indexgI K) Lagrange_index ?indexgS ?subsetIl ?subsetIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)