feat(order/bounded_lattice): min/max commute with coe (#6900)
feat(order/bounded_lattice): min/max commute with coe (#6900)

to with_bot and with_top





Co-authored-by: Floris van Doorn <240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu>

leanprover-community/mathlib,leanprover-community/mathlib