fact: Definition subgroup_index {U : Univalence} (G : Group) (H : Subgroup G) (fin_G : Finite G) (fin_H : Finite H) : nat.
imports: Basics Types Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.QuotientGroup Spaces.Finite.Finite Spaces.Nat.Core