proposition: Lemma indexg_gt0 A : 0 < #|G : A|.
proof: Proof. rewrite lt0n; apply/existsP; exists A. by rewrite -{2}[A]mulg1 -rcosetE; apply: imset_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)