asym_spec_struct_A

import Mathlib.Algebra.Order.Ring.Defs

universe u

structure SemiringPreorder_A (α : Type u) [CommSemiring α] extends Preorder α where
  add_right : ∀ a b, le a b → ∀ c, le (a + c) (b + c)
  mul_right : ∀ a b, le a b → ∀ c, le (a * c) (b * c)
  zero_le   : ∀ a : α, le 0 a