mathlib3

3026899c - feat(algebra/order/monoid/with_top): add `with_top/bot.coe_pos` (#17651)

feat(algebra/order/monoid/with_top): add `with_top/bot.coe_pos` (#17651) * Add `with_top.one_lt_coe`, `with_bot.one_lt_coe`, `with_top.coe_pos`, and `with_bot.coe_pos`. * Add `with_top.coe_lt_one`, `with_bot.coe_lt_one`, `with_top.coe_neg`, and `with_bot.coe_neg`. * Use `with_bot.coe_pos` to golf a proof.