proposition: Lemma index2_normal G H : H \subset G -> #|G : H| = 2 -> H <| G.
proof: Proof. move=> sHG indexHG; rewrite /normal sHG; apply/subsetP=> x Gx. case Hx: (x \in H); first by rewrite inE conjGid. rewrite inE conjsgE mulgA -sub_rcosetV -invg_rcoset. by rewrite !(rcoset_index2 sHG) ?inE ?groupV ?Hx // invDg !invGid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)