\import Algebra.Monoid
\import Order.PartialOrder
\import Paths

\class OrderedMonoid \extends Poset, Monoid {
  | <=_*-left (z : E) {x y : E} : x <= y -> x * z <= y * z
  | <=_*-right (z : E) {x y : E} : x <= y -> z * x <= z * y

  \lemma <=_* {a b c d : E} (p : a <= c) (q : b <= d) : a * b <= c * d
    => <=_*-left b p <=∘ <=_*-right c q
}

\class OrderedCMonoid \extends OrderedMonoid, CMonoid
  | <=_*-right z x<y => transport2 (<=) *-comm *-comm (<=_*-left z x<y)