proposition: Lemma indexg_eq1 G H : (#|G : H| == 1%N) = (G \subset H).
proof: Proof. rewrite eqn_leq -(leq_pmul2l (cardG_gt0 (G :&: H))) LagrangeI muln1. by rewrite indexg_gt0 andbT (sameP setIidPl eqP) eqEcard subsetIl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)