∀ {S : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : GroupConeClass S G],
  PartialOrder.mkOfGroupCone C =
    { le := fun a b => b / a ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }