asym_spec_struct_E

import Mathlib.Algebra.Order.Ring.Defs

universe u

structure StrassenPreorder_E (α : Type u) [CommSemiring α] extends Preorder α where
  add_right : ∀ a b, le a b → ∀ c, le (a + c) (b + c)

namespace StrassenPreorder_E

variable {α : Type u} [CommSemiring α]

def activate (P : StrassenPreorder_E α) (f : [Preorder α] → β) : β :=
  letI : Preorder α := P.toPreorder
  f

end StrassenPreorder_E