proposition: Lemma natf_indexg (gT : finGroupType) (G H : {group gT}) : H \subset G -> #|G : H|%:R = (#|G|%:R / #|H|%:R)%R :> F.
proof: Proof. by move=> sHG; rewrite -divgS // natf_div ?cardSg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)