asym_spec_struct_D

import Mathlib.Algebra.Order.Ring.Defs

universe u

structure SemiringPreorder_D (α : 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_D (α : Type u) [CommSemiring α] extends SemiringPreorder_D α 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 StrassenPreorder_D

variable {α : Type u} [CommSemiring α]

def activate (P : StrassenPreorder_D α) (f : [Preorder α] → [CovariantClass α α (· + ·) (· ≤ ·)] → [PosMulMono α] → [MulPosMono α] → β) : β :=
  letI : Preorder α := P.toPreorder
  letI : CovariantClass α α (· + ·) (· ≤ ·) := ⟨fun a _ _ bc ↦ by
    rw [add_comm a, add_comm a]
    exact P.add_right _ _ bc a⟩
  letI : PosMulMono α := ⟨fun x _ _ _ h ↦ by
    rw [mul_comm x, mul_comm x]
    exact P.mul_right _ _ h x⟩
  letI : MulPosMono α := ⟨fun x _ _ _ h ↦ P.mul_right _ _ h x⟩
  f

end StrassenPreorder_D