Commit 2022-11-28 20:12 5c8f8804

feat: port Algebra.Order.Monoid.Defs (#771) from mathlib3port 76171581280d5b5d1e2d1f4f37e5420357bdc636 The structure definitions and instances already existed, in the placeholder file Algebra.Order.Monoid; just a couple of lemmas needed to be ported. The remaining material in the placeholder file Algebra.Order.Monoid was about ordered-cancel-monoids, so I have moved this to a new placeholder file Algebra.Order.Monoid.Cancel (itself to be replaced eventually by Algebra.Order.Monoid.Cancel.*). I commented out the lemma

theorem bit0_pos [OrderedAddCommMonoid α] {a : α} (h : 0 < a) : 0 < bit0 a :=
  add_pos' h h

was this the right move or should I have deleted it? Or kept and labelled as a nolint?