Unbundled ordered monoid structures on the order dual.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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