{R : Type u} →
  [inst : NonAssocSemiring R] →
    (carrier : Set R) →
      (∀ {a b : R}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier) →
        1 ∈ carrier → (∀ {a b : R}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier) → 0 ∈ carrier → Subsemiring R