mathlib3

cf7b16a6 - chore(algebra/order/monoid): move lemmas (#16176)

chore(algebra/order/monoid): move lemmas (#16176) * move `with_top.coe_nat` to `algebra.order.monoid`, prove by `rfl`; * move `with_top.nat_ne_top` and `with_top.top_ne_nat` to `algebra.order.monoid`; * add `with_bot` versions.