{R : Type u_2} →
  [inst : NonUnitalNonAssocRing R] →
    (toFun : R → ℝ) →
      toFun 0 = 0 →
        (∀ (r s : R), toFun (r + s) ≤ toFun r + toFun s) →
          (∀ (r : R), toFun (-r) = toFun r) → (∀ (x y : R), toFun (x * y) ≤ toFun x * toFun y) → RingSeminorm R