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