∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (M N : AddSubgroup R) (r₁ r₂ : R),
  -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier →
    -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier → -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier