∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  autoParam (∀ (a b : SeparationQuotient G), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam