proposition: Lemma rcoset_index2 G H x : H \subset G -> #|G : H| = 2 -> x \in G :\: H -> H :* x = G :\: H.
proof: Proof. move=> sHG indexHG => /setDP[Gx notHx]; apply/eqP. rewrite eqEcard -(leq_add2l #|G :&: H|) cardsID -(LagrangeI G H) indexHG muln2. rewrite (setIidPr sHG) card_rcoset addnn leqnn andbT. apply/subsetP=> _ /rcosetP[y Hy ->]; apply/setDP. by rewrite !groupMl // (subsetP sHG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)