Prove algebraic class of subtype via closure

Stream: mathlib4

[Bolton Bailey]

I would like to complete

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Degree.Definitions

def TropicallyBoundPolynomials (R) [Semiring R] : Type :=
{ p : (Polynomial R × Tropical (OrderDual ℕ)) // p.1.natDegree ≤ p.2.untrop }

instance [Semiring R] : Semiring (TropicallyBoundPolynomials R) := by
  sorry

Is there some way I can do this just by proving that the subtype is closed under 0, + and *?

[Junyan Xu]

Construct a docs#Subsemiring with the set
{ p : (Polynomial R × Tropical (OrderDual ℕ)) | p.1.natDegree ≤ p.2.untrop }
as the carrier, and it automatically gets a Semiring instance.

[Bolton Bailey]

Hmm, unfortunately this turned out not to be a Semiring like I thought. Is there something similar for Distrib?

[Kevin Buzzard]

I'm afraid mathlib doesn't have subdistribs. But distrib is a Prop-valued class so what even would that mean?

[Eric Wieser]

But distrib is a Prop-valued class

No it isn't: docs#Distrib