asym_spec_struct_B

import Mathlib.Algebra.Order.Ring.Defs
import Mathlib.Algebra.CharZero.Defs
import Mathlib.Tactic.Ext

universe u

structure SemiringPreorder_B (α : 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

structure StrassenPreorder_B (α : Type u) [CommSemiring α] extends SemiringPreorder_B α where
  nat_order_embedding : ∀ n m : ℕ, le (n : α) (m : α) ↔ n ≤ m
  lower_archimedean : ∀ a : α, a = 0 ∨ le 1 a
  upper_archimedean : ∀ a : α, ∃ n : ℕ, le a (n : α)

namespace SemiringPreorder_B

variable {α : Type u} [CommSemiring α]

instance : PartialOrder (SemiringPreorder_B α) where
  le P Q := ∀ a b, P.le a b → Q.le a b
  le_refl P a b h := h
  le_trans P Q R hPQ hQR a b h := hQR _ _ (hPQ _ _ h)
  le_antisymm P Q hPQ hQP := by
    cases P; cases Q
    congr
    · ext a b
      exact ⟨hPQ a b, hQP a b⟩

end SemiringPreorder_B