Unbundled ordered monoid structures on the order dual.

instance OrderDual.mulLeftReflectLE {α : Type u} [LE α] [Mul α] [c : MulLeftReflectLE α] : MulLeftReflectLE αᵒᵈ

instance OrderDual.addLeftReflectLE {α : Type u} [LE α] [Add α] [c : AddLeftReflectLE α] : AddLeftReflectLE αᵒᵈ

instance OrderDual.mulLeftMono {α : Type u} [LE α] [Mul α] [c : MulLeftMono α] : MulLeftMono αᵒᵈ

instance OrderDual.addLeftMono {α : Type u} [LE α] [Add α] [c : AddLeftMono α] : AddLeftMono αᵒᵈ

instance OrderDual.mulRightReflectLE {α : Type u} [LE α] [Mul α] [c : MulRightReflectLE α] : MulRightReflectLE αᵒᵈ

instance OrderDual.addRightReflectLE {α : Type u} [LE α] [Add α] [c : AddRightReflectLE α] : AddRightReflectLE αᵒᵈ

instance OrderDual.mulRightMono {α : Type u} [LE α] [Mul α] [c : MulRightMono α] : MulRightMono αᵒᵈ

instance OrderDual.addRightMono {α : Type u} [LE α] [Add α] [c : AddRightMono α] : AddRightMono αᵒᵈ

instance OrderDual.mulLeftReflectLT {α : Type u} [LT α] [Mul α] [c : MulLeftReflectLT α] : MulLeftReflectLT αᵒᵈ

instance OrderDual.addLeftReflectLT {α : Type u} [LT α] [Add α] [c : AddLeftReflectLT α] : AddLeftReflectLT αᵒᵈ

instance OrderDual.mulLeftStrictMono {α : Type u} [LT α] [Mul α] [c : MulLeftStrictMono α] : MulLeftStrictMono αᵒᵈ

instance OrderDual.addLeftStrictMono {α : Type u} [LT α] [Add α] [c : AddLeftStrictMono α] : AddLeftStrictMono αᵒᵈ

instance OrderDual.mulRightReflectLT {α : Type u} [LT α] [Mul α] [c : MulRightReflectLT α] : MulRightReflectLT αᵒᵈ

instance OrderDual.addRightReflectLT {α : Type u} [LT α] [Add α] [c : AddRightReflectLT α] : AddRightReflectLT αᵒᵈ

instance OrderDual.mulRightStrictMono {α : Type u} [LT α] [Mul α] [c : MulRightStrictMono α] : MulRightStrictMono αᵒᵈ

instance OrderDual.addRightStrictMono {α : Type u} [LT α] [Add α] [c : AddRightStrictMono α] : AddRightStrictMono αᵒᵈ