∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (x y : M),
  (↑SeparationQuotient.mkAddMonoidHom).toFun (x + y) =
    (↑SeparationQuotient.mkAddMonoidHom).toFun x + (↑SeparationQuotient.mkAddMonoidHom).toFun y