∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  [inst_3 : H.Normal], (Nat.card ↥H).Coprime H.index → ∀ (α : H.QuotientDiff) (h : ↥H), h • α = α → h = 1