∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [inst_2 : IsTopologicalRing R]
  (a b : R), SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b